- 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 6a1bee0c7f9f6cd601925933200a5887fdd7dda3..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
@@ -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))))).