(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
-(* Main properties about atomic arity assignment on terms *******************)
+(* Main inversion lemmas about atomic arity assignment on terms *************)
theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →