proposition: Lemma eqb_spec : forall t1 t2, eqb t1 t2 <-> t1 = t2.
proof: Proof. intros;symmetry; apply reflect_iff; apply reflect_eqb. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList