ground_2 released and permanently renamed as ground

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
index 776affc1c95b4f3fda5e8dddb22ef4bb39424c59..e127fa23654f19aab07b5687cb781ae25b8b4fe8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/xoa/ex_3_4.ma".
-include "ground_2/xoa/ex_4_1.ma".
+include "ground/xoa/ex_3_4.ma".
+include "ground/xoa/ex_4_1.ma".
 include "static_2/notation/relations/voidstareq_4.ma".
 include "static_2/syntax/lenv.ma".
 
@@ -96,7 +96,7 @@ 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.
+lemma lveq_inv_bind_O: ∀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-.