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