proposition: Lemma reflect_eqb : forall t1 t2, reflect (t1 = t2) (eqb t1 t2).
proof: Proof. destruct t1;destruct t2;simpl; try (constructor;trivial;discriminate). preflect (reflect_cop_eqb c c0);constructor;subst;trivial. preflect (reflect_uop_eqb u u0); preflect (Misc.reflect_eqb i i0); constructor;subst;trivial. preflect (reflect_bop_eqb b b0); preflect (Misc.reflect_eqb i i1); preflect (Misc.reflect_eqb i0 i2); constructor;subst;trivial. preflect (reflect_top_eqb t t0). preflect (Misc.reflect_eqb i i2). preflect (Misc.reflect_eqb i0 i3). preflect (Misc.reflect_eqb i1 i4). constructor;subst;trivial. preflect (reflect_nop_eqb n n0); preflect (reflect_list_beq _ _ Misc.reflect_eqb l l0); constructor; subst; reflexivity. preflect (Misc.reflect_eqb i i0); preflect (reflect_list_beq _ _ Misc.reflect_eqb l l0); constructor;subst;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList