proposition: Lemma reflect_bop_eqb : forall o1 o2, reflect (o1 = o2) (bop_eqb o1 o2).
proof: Proof. intros [ | | | | | | | A1|s1|s1 |s1 | s1 | s1 | s1 | s1 | s1 | s1 | s1 | I1 E1 | I1 E1 ] [ | | | | | | | A2|s2|s2| s2 | s2 | s2 | s2 | s2 | s2 | s2 | s2 |I2 E2 | I2 E2 ]; simpl;try (constructor;trivial;discriminate). - preflect (Typ.reflect_eqb A1 A2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - intros. preflect (N.eqb_spec s1 s2). preflect (N.eqb_spec n n0). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (N.eqb_spec s1 s2). constructor;subst;trivial. - preflect (Typ.reflect_eqb I1 I2). preflect (Typ.reflect_eqb E1 E2). constructor;subst;trivial. - preflect (Typ.reflect_eqb I1 I2). preflect (Typ.reflect_eqb E1 E2). constructor;subst;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList