Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma
index 16393b04b8ae309b703cc2ab273f7a6a21fd8d6a..549441f261f7d9d3364b17a02aeb7ef91491ba9a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma
@@ -232,7 +232,7 @@ is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g (AHead a1 a2) c2
 (lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H4: 
 (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H5: (csubc g d1 c2)).(let H_y 
 \def (H1 d1 is H4 c2 H5) in (let H_y0 \def (H3 d1 is H4 c2 H5) in (let H6 
-\def H_y0 in (and_ind (arity g c2 (lift1 is t0) (AHead a1 a2)) (\forall (d: 
+\def H_y0 in (land_ind (arity g c2 (lift1 is t0) (AHead a1 a2)) (\forall (d: 
 C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0: PList).((drop1 is0 d 
 c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is t0))))))))) 
 (sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))) (\lambda (_: (arity g c2