two cases of cpx_lfxs_conf_fle closed

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / lveq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma
index e19708385f8b7d4fbcfdff2d99a4e7a5844adae3..524c2779b38549936a581c24d053cd8ccbdd490c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma
@@ -94,6 +94,11 @@ lemma lveq_inv_succ: ∀L1,L2,n1,n2. L1 ≋ⓧ*[⫯n1, ⫯n2] L2 → ⊥.
 
 (* Advanced inversion lemmas ************************************************)
 
+lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ{I1} ≋ⓧ*[0, 0] K2.ⓘ{I2} → K1 ≋ⓧ*[0, 0] K2.
+#I1 #I2 #K1 #K2 #H
+elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct //
+qed-.
+  
 lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1, n2] ⋆ → ∧∧ 0 = n1 & 0 = n2.
 * [2: #n1 ] * [2,4: #n2 ] #H
 [ elim (lveq_inv_succ … H)