proposition: Lemma assert_beq_list : forall A eq, forall l1 l2 : list A, assert (beq_list eq l1 l2) <=> l1 = l2.
proof: Proof. induction l1; destruct l2; simpl; split; sp; try (complete (inversion H)). destruct (eq a a0); subst. f_equal. apply IHl1; auto. inversion H. inversion H; subst. destruct (eq a0 a0); subst; sp. apply IHl1; sp. Qed.
imports: UsefulTypes bin_rels Omega