(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* Properties concerning generic relocation *********************************)
lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* Properties concerning generic relocation *********************************)
lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →