proposition: Lemma snoc_cases : forall T, forall l : list T, l = [] [+] {a : T $ {k : list T $ l = snoc k a}}.
proof: Proof. induction l. left; auto. sp; subst. right; exists a; exists (@nil T); simpl; auto. right. exists a0; exists (a :: k); simpl; auto. Qed.
imports: UsefulTypes bin_rels Omega