(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/props".
+include "LambdaDelta-1/pc1/defs.ma".
-include "pc1/defs.ma".
-
-include "pr1/pr1.ma".
+include "LambdaDelta-1/pr1/pr1.ma".
theorem pc1_pr0_r:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
(\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1)
(pr1_pr0 t2 t1 H)))).
+theorem pc1_refl:
+ \forall (t: T).(pc1 t t)
+\def
+ \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0:
+T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
+
theorem pc1_pr0_u:
\forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2
t3) \to (pc1 t1 t3)))))
(t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2)
H3)))) H1)))))).
-theorem pc1_refl:
- \forall (t: T).(pc1 t t)
-\def
- \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0:
-T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
-
theorem pc1_s:
\forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
\def