proposition: Lemma reflect_list_beq : forall (A:Type) (beq:A -> A -> bool), (forall x y, reflect (x = y) (beq x y)) -> forall x y, reflect (x = y) (list_beq beq x y).
proof: Proof. intros A beq Hbeq;induction x;destruct y;simpl;try (constructor;trivial;discriminate). destruct (Hbeq a a0) as [Heq | Hd];simpl;[ | constructor;intros Heq;elim Hd;inversion Heq;trivial]. destruct (IHx y) as [Heq0 | Hd];simpl;[ | constructor;intros Heq0;elim Hd;inversion Heq0;trivial]. constructor;subst;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList