(* *)
(**************************************************************************)
-include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/relocation/ldrop_ldrop.ma".
include "basic_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* Main properties **********************************************************)
-theorem aaa_mono: ∀L,T,A1. L ⊢ T ⁝ A1 → ∀A2. L ⊢ T ⁝ A2 → A1 = A2.
+theorem aaa_mono: ∀L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
#L #T #A1 #H elim H -L -T -A1
[ #L #k #A2 #H
>(aaa_inv_sort … H) -H //