∀Ts,Us. ⬆*[f] Ts ≡ Us →
all … (R K) Ts → all … (R L) Us.
(* Properties with generic relocation for term vectors **********************)
(* Basic_2A1: was: d1_liftables_liftables_all *)
∀Ts,Us. ⬆*[f] Ts ≡ Us →
all … (R K) Ts → all … (R L) Us.
(* Properties with generic relocation for term vectors **********************)
(* Basic_2A1: was: d1_liftables_liftables_all *)