is there any tactic in Coq that can transform a bool expression to a Prop one?

Question

For example, I have this hypothesis in my context:

Heq: (a =? b) &&
     (c =? d) &&
     (e =? f) = true

that I would like to transform to this:

Heq: (a = b) /\
     (c = d) /\
     (e = f)

I have seen this post coq tactic for replacing bools with Prop but it was not really strightforward to me to use those tactics because there is no Is_true in the expression in my context.

Edit:

Heq is modified by adding = true since I made a mistake first time reading it from the context.

Answer 1

I have solved it by:

apply Bool.andb_true_iff in Heq.

which adds = true to the last two bool expressions and replace the second && with /\.

I then split the Heq expression into two sub-expressions by:

destruct Heq as (HeqA & HeqB).

and did the same thing on the remaining left bool sub-expression:

apply Bool.andb_true_iff in HeqA. 
destruct HeqA as (HeqA & HeqC).

Finally, I converted the bool equality into Prop equality by:

apply beq_nat_true in HeqA.
apply beq_nat_true in HeqB.
apply beq_nat_true in HeqC.