proposition: Lemma deq_list {A} (deq : Deq A): Deq (list A).
proof: Proof. intro lx. induction lx as [| x lx Hind]; intro ly; destruct ly as [| y ly];sp;[right|right |];sp;[]. destruct (Hind ly); destruct (deq x y); subst; sp; right; introv Heq; inverts Heq; sp. Qed.
imports: UsefulTypes bin_rels Omega