(* *)
(**************************************************************************)
+include "ground/xoa/ex_5_3.ma".
+include "ground/xoa/ex_6_4.ma".
include "basic_2A/notation/relations/lrsubeqa_3.ma".
include "basic_2A/static/lsubr.ma".
include "basic_2A/static/aaa.ma".
]
qed-.
-lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
+lemma lsuba_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆.
/2 width=4 by lsuba_inv_atom2_aux/ qed-.
fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →