(* Main properties about atomic arity assignment on terms *******************)
theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 →
- ∀T,A1. L1 ⊢ T ÷ A1 → ∀A2. L2 ⊢ T ÷ A2 →
+ ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 →
A1 = A2.
#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2
elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2
qed-.
theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 →
- ∀A1. L ⊢ T1 ÷ A1 → ∀A2. L ⊢ T2 ÷ A2 →
+ ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 →
A1 = A2.
#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2
elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2