- some bugs fixed in the domain-based preorders on environments

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / pc1 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma
index caa38f0fc57637db90c300dfcb68df3c428a8fde..a156a65b44d9308a7066709d05d691bd3de06a83 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "pc1/defs.ma".
+include "LambdaDelta-1/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)))
@@ -32,6 +32,12 @@ theorem pc1_pr0_x:
 (\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)))))
@@ -43,12 +49,6 @@ T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda
 (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