milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lsubr_lsubr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma
index 426166ab6657b3eedf3de9747d07978d737d6391..98f32272240d691a551f880ede10f0a1c3f8ea91 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma
@@ -16,6 +16,8 @@ include "basic_2/substitution/lsubr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
+(* Auxiliary inversion lemmas ***********************************************)
+
 fact lsubr_inv_abbr1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓓW →
                           ∨∨ L2 = ⋆
                            | ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓓW