proposition: Lemma app_cons_not_nil : forall (A : Type) (y : A) (xs ys : list A), xs ++ y :: ys <> nil.
proof: Proof. intros ? ? ? ? H. symmetry in H. revert H. apply List.app_cons_not_nil. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac