(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/tinycals".
+
theorem prova:
- \forall A,B:Prop.
- \forall H:A \to A \to A \to A \to A \to B.A \to B.
+ \forall A,B,C:Prop.
+ \forall H:A \to A \to C \to A \to A \to B.A \to C \to B.
intros.
apply H;
[assumption
- |3,5:assumption;
- 4:assumption
+ |3,5:
+ [ exact H2;
+ | exact H1 ]
+ |4:assumption
|*:assumption
]
qed.
\forall H:A \to A \to A \to A \to A \to B.A \to B.
intros.
apply H;
- [*:assumption
- ]
+ [*:assumption]
qed.
+include "logic/connectives.ma".
+
theorem prova2:
\forall A,B:Prop.
- \forall H:A \to A \to A \to A \to A \to B.A \to B.
+ \forall H:A \to A \to A \to (A \land A) \to A \to B.A \to B.
intros.
apply H;
[2:assumption
- |assumption
- 3,5:assumption
- *:assumption
+ |4:split.assumption
+ |3,5:assumption
+ |*:assumption
]
+assumption.
qed.