cicNotationPp: fixed letin syntax (now typeless)

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

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 1ad44c87adf66bea3cbcbdd5685617dd5352b779..4a240f89887750db652196751b7c146f7bb49061 100644 (file)
--- 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).