proposition: Lemma length1 : forall T, forall l : list T, length l = 1 <=> {x : T $ l = [x]}.
proof: Proof. destruct l; simpl; sp. split; sp; inversion H. split; sp; try (inversion H); subst. destruct l; simpl in H1; inversion H1. exists t; auto. invs; sp. Qed.
imports: UsefulTypes bin_rels Omega