proposition: Theorem eq_list : forall (A : Type) (x : A) (l1 l2 : list A), l1 = l2 <=> length l1 = length l2 # (forall n : nat, nth n l1 x = nth n l2 x).
proof: Proof. intros. apply eq_lists. Qed.
imports: UsefulTypes bin_rels Omega