Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
index 57e9f7ef1594058fd4548d643ebea495e7eecbcf..2e70987d71a91f98f29fcf4b287680067de66cf0 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma
@@ -256,7 +256,7 @@ t3 w)).(\lambda (t4: T).(\lambda (H0: (pr0 (lift (S O) O t4) t3)).(\lambda
 O) O x))).(\lambda (_: (pr0 t4 x)).(let H3 \def (eq_ind T t3 (\lambda (t: 
 T).(subst0 O u2 t w)) H (lift (S O) O x) H1) in (subst0_gen_lift_false x u2 w 
 (S O) O O (le_n O) (eq_ind_r nat (plus (S O) O) (\lambda (n: nat).(lt O n)) 
-(le_n (plus (S O) O)) (plus O (S O)) (plus_comm O (S O))) H3 (ex2 T (\lambda 
+(le_n (plus (S O) O)) (plus O (S O)) (plus_sym O (S O))) H3 (ex2 T (\lambda 
 (t: T).(pr0 (THead (Bind Abbr) u2 w) t)) (\lambda (t: T).(pr0 t2 t)))))))) 
 (pr0_gen_lift t4 t3 (S O) O H0)))))))).