proposition: Lemma nil_snoc_false : forall T, forall a : list T, forall b : T, [] = snoc a b -> False.
proof: Proof. intros. assert (length ([] : list T) = length (snoc a b)). rewrite H; auto. simpl in H0. rewrite length_snoc in H0. inversion H0. Qed.
imports: UsefulTypes bin_rels Omega