proposition: Lemma rev_list_dest : forall T, forall l : list T, l = [] [+] {u : list T $ {v : T $ l = snoc u v}}.
proof: Proof. induction l using rev_list_indT. left; auto. right; auto. exists l a; auto. Qed.
imports: UsefulTypes bin_rels Omega