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

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / pr0 / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma
index e6ca5293d6e473521c7386bf7282fd597e2edc1a..7ad8f8eef4b91e477625c9ad3f158224428075f8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma
@@ -1950,7 +1950,7 @@ x2))).(\lambda (H7: (eq T (lift (S O) O t2) (lift h (S x1) x3))).(eq_ind_r T
 (THead (Bind b) x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t3 (lift 
 h x1 t4))) (\lambda (t4: T).(pr0 t t4)))) (let H8 \def (eq_ind_r nat (plus (S 
 O) x1) (\lambda (n: nat).(eq nat (S x1) n)) (refl_equal nat (plus (S O) x1)) 
-(plus x1 (S O)) (plus_comm x1 (S O))) in (let H9 \def (eq_ind nat (S x1) 
+(plus x1 (S O)) (plus_sym x1 (S O))) in (let H9 \def (eq_ind nat (S x1) 
 (\lambda (n: nat).(eq T (lift (S O) O t2) (lift h n x3))) H7 (plus x1 (S O)) 
 H8) in (ex2_ind T (\lambda (t4: T).(eq T x3 (lift (S O) O t4))) (\lambda (t4: 
 T).(eq T t2 (lift h x1 t4))) (ex2 T (\lambda (t4: T).(eq T t3 (lift h x1 
@@ -1988,7 +1988,7 @@ t3 (lift h x1 x4))).(\lambda (H7: (pr0 x3 x4)).(eq_ind_r T (lift h x1 x4)
 (\lambda (t: T).(ex2 T (\lambda (t4: T).(eq T t (lift h x1 t4))) (\lambda 
 (t4: T).(pr0 (THead (Flat Cast) x2 x3) t4)))) (ex_intro2 T (\lambda (t4: 
 T).(eq T (lift h x1 x4) (lift h x1 t4))) (\lambda (t4: T).(pr0 (THead (Flat 
-Cast) x2 x3) t4)) x4 (refl_equal T (lift h x1 x4)) (pr0_epsilon x3 x4 H7 x2)) 
-t3 H_x)))) (H2 x3 x1 H6)) x0 H4)))))) (lift_gen_flat Cast u t2 x0 h x1 
+Cast) x2 x3) t4)) x4 (refl_equal T (lift h x1 x4)) (pr0_tau x3 x4 H7 x2)) t3 
+H_x)))) (H2 x3 x1 H6)) x0 H4)))))) (lift_gen_flat Cast u t2 x0 h x1 
 H3)))))))))) y x H0))))) H))))).