X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr0%2Fdec.ma;h=4a240f89887750db652196751b7c146f7bb49061;hb=3b2361afb73203749541ad07e94648da6057ae67;hp=1ad44c87adf66bea3cbcbdd5685617dd5352b779;hpb=413007de240fefb28650bb5ba7940f46db656751;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
index 1ad44c87a..4a240f898 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma
@@ -521,6 +521,6 @@ Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead
 (Flat Cast) t t0) t2))) (ex_intro2 T (\lambda (t2: T).((eq T (THead (Flat 
 Cast) t t0) t2) \to (\forall (P: Prop).P))) (\lambda (t2: T).(pr0 (THead 
 (Flat Cast) t t0) t2)) t0 (\lambda (H1: (eq T (THead (Flat Cast) t t0) 
-t0)).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) t t0 H1 P))) (pr0_epsilon t0 
-t0 (pr0_refl t0) t))) f)) k)))))) t1).
+t0)).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) t t0 H1 P))) (pr0_tau t0 t0 
+(pr0_refl t0) t))) f)) k)))))) t1).