proposition: Lemma list_beq_spec : forall (A:Type) (beq:A -> A -> bool), (forall x y, beq x y <-> x = y) -> forall x y, list_beq beq x y <-> x = y.
proof: Proof. intros A beq HA x y;symmetry;apply reflect_iff;apply reflect_list_beq. intros;apply iff_reflect;symmetry;apply HA. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList