set "baseuri" "cic:/matita/tests/metasenv_ordering".
-include "coq.ma".
+include "legacy/coq.ma".
alias num (instance 0) = "natural number".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
\forall P:Prop.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 2 = 2.
- intros. split. split.
- goal 13.
- rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].
- reflexivity.
- reflexivity.
+ intros. split; split;
+ [ reflexivity
+ | rewrite > H;
+ [ reflexivity | exact nat | exact (0=0) | exact Type ]
+ ]
qed.
theorem th2 :
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 3 = 3.
intros. split. split.
- goal 13.
- rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 4 = 4.
intros. split. split.
- goal 13.
- rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 5 = 5.
intros. split. split.
- goal 13.
- rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 6 = 6.
intros. split. split.
- goal 13.
- apply H; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply H; [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 7 = 7.
intros. split. split.
- goal 13.
- apply H ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 8 = 8.
intros. split. split.
- goal 13.
- apply H ? ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ? ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 9 = 9.
intros. split. split.
- goal 13.
- apply H ? ? ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
theorem th9:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
- elim H ? ?; [split; assumption | exact r | exact s].
+ intros (P Q R S r s H).
+ elim (H ? ?); [split; assumption | exact r | exact s].
qed.
theorem th10:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
- elim H ?; [split; assumption | exact r | exact s].
+ intros (P Q R S r s H).
+ elim (H ?); [split; assumption | exact r | exact s].
qed.
theorem th11:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
+ intros (P Q R S r s H).
elim H; [split; assumption | exact r | exact s].
qed.
-
-
-
-
-
-
-
-
-
-
\ No newline at end of file