proposition: Lemma eq_lists : forall A (l1 l2 : list A) x, l1 = l2 <=> ( length l1 = length l2 # forall n, nth n l1 x = nth n l2 x ).
proof: Proof. induction l1; sp; destruct l2; sp; split; allsimpl; sp; try(inversion H);try(inversion H0); subst; sp. gen_some 0; subst. assert (l1 = l2) as eq; try (rewrite eq; sp). apply IHl1 with (x := x); sp. gen_some (S n); sp. Qed.
imports: UsefulTypes bin_rels Omega