proposition: Lemma length2 : forall (T : Type) (l : list T), length l = 2 -> {x, y : T $ l = [x,y]}.
proof: Proof. introv Hl. destruct l; try(destruct l); try(destruct l); inverts Hl. eexists; eauto. Qed.
imports: UsefulTypes bin_rels Omega