update in ground_2, static_2, basic_2

[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 e6d2fcbfc37a30a8714ffa23f1451faf90f02da6..a895a58112277d5adb3bec01e88b9fa6f8873959 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/lveq.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_3_4.ma".
+include "ground_2/xoa/ex_4_1.ma".
 include "static_2/notation/relations/voidstareq_4.ma".
 include "static_2/syntax/lenv.ma".
 
@@ -98,7 +100,7 @@ lemma lveq_inv_bind: ∀I1,I2,K1,K2. K1.ⓘ{I1} ≋ⓧ*[0,0] K2.ⓘ{I2} → K1 
 #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)