cicInspect: now we can choose not to count the Cic.Implicit constructors

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
index 7e7f6a80a3cc3c49823ef4ad560ddc2b41bc7aa9..8f399a0fd18042df184855254df61a5db610e551 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma
@@ -114,14 +114,14 @@ t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t))))
 (eq_ind_r nat (plus (trans hds0 i) h) (\lambda (n: nat).(eq T (lift (S n) O 
 (lift1 (ptrans hds0 i) t)) (lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans 
 hds0 i) t)))) (refl_equal T (lift (S (plus (trans hds0 i) h)) O (lift1 
-(ptrans hds0 i) t))) (plus h (trans hds0 i)) (plus_comm h (trans hds0 i))) 
+(ptrans hds0 i) t))) (plus h (trans hds0 i)) (plus_sym h (trans hds0 i))) 
 (plus h (S (trans hds0 i))) (plus_n_Sm h (trans hds0 i))) (lift h d (lift (S 
 (trans hds0 i)) O (lift1 (ptrans hds0 i) t))) (lift_free (lift1 (ptrans hds0 
 i) t) (S (trans hds0 i)) h O d (eq_ind nat (S (plus O (trans hds0 i))) 
 (\lambda (n: nat).(le d n)) (eq_ind_r nat (plus (trans hds0 i) O) (\lambda 
 (n: nat).(le d (S n))) (le_S d (plus (trans hds0 i) O) (le_plus_trans d 
 (trans hds0 i) O (bge_le d (trans hds0 i) H0))) (plus O (trans hds0 i)) 
-(plus_comm O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans 
+(plus_sym O (trans hds0 i))) (plus O (S (trans hds0 i))) (plus_n_Sm O (trans 
 hds0 i))) (le_O_n d)))) x_x))) (lift1 hds0 (lift (S i) O t)) (H i t)))))))) 
 hds).