]>
matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/apply.ma
theorem b:
\forall x:Prop.
(not x) \to x \to False.
-intro.
+intros.
apply H.
assumption.
qed.
\forall A:Set.
\forall x,y : A.
not (x=y) \to not (x=y).
-intro.
+intros.
apply H.
qed.