proposition: Lemma in_not_nil_42 : forall l : list nat, In 42 l -> l <> [].
proof: Proof. intros l H. Fail apply in_not_nil. Abort. Lemma in_not_nil_42_take2 : forall l : list nat, In 42 l -> l <> []. Proof. intros l H. apply in_not_nil with (x := 42). apply H. Qed.