1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/tests/metasenv_ordering".
19 alias num (instance 0) = "natural number".
20 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
26 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
27 1 = 1 \land 1 = 0 \land 2 = 2.
30 rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].
37 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
38 1 = 1 \land 1 = 0 \land 3 = 3.
41 rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].
48 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
49 1 = 1 \land 1 = 0 \land 4 = 4.
52 rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
59 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
60 1 = 1 \land 1 = 0 \land 5 = 5.
63 rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
72 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
73 1 = 1 \land 1 = 0 \land 6 = 6.
76 apply H; [exact nat | exact 0=0 | exact Type].
83 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
84 1 = 1 \land 1 = 0 \land 7 = 7.
87 apply H ?; [exact nat | exact 0=0 | exact Type].
94 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
95 1 = 1 \land 1 = 0 \land 8 = 8.
98 apply H ? ?; [exact nat | exact 0=0 | exact Type].
105 \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
106 1 = 1 \land 1 = 0 \land 9 = 9.
107 intros. split. split.
109 apply H ? ? ?; [exact nat | exact 0=0 | exact Type].
117 \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
118 intros [P; Q; R; S; r; s; H].
119 elim H ? ?; [split; assumption | exact r | exact s].
123 \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
124 intros [P; Q; R; S; r; s; H].
125 elim H ?; [split; assumption | exact r | exact s].
129 \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
130 intros [P; Q; R; S; r; s; H].
131 elim H; [split; assumption | exact r | exact s].