(* *)
(**************************************************************************)
+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".
#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)