eq over SET1 and SET no longer used

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma
index 867542f5a5887afc57b304d9a043f6406a5b53d9..159e6d5e7f7061a6bee287adb7fd3a719b702535 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma
@@ -162,6 +162,14 @@ theorem pc3_pr2_u2:
 t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x 
 c t1 t0 H) t2 H0)))))).
 
+theorem pc3_pr3_conf:
+ \forall (c: C).(\forall (t: T).(\forall (t1: T).((pc3 c t t1) \to (\forall 
+(t2: T).((pr3 c t t2) \to (pc3 c t2 t1))))))
+\def
+ \lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t 
+t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c 
+t2 t H0) t1 H)))))).
+
 theorem pc3_head_12:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall 
 (k: K).(\forall (t1: T).(\forall (t2: T).((pc3 (CHead c k u2) t1 t2) \to (pc3