include "apps_2/functional/notation.ma".
(* FUNCTIONAL RELOCATION ****************************************************)
include "apps_2/functional/notation.ma".
(* FUNCTIONAL RELOCATION ****************************************************)
-theorem flift_lift: â\88\80T,d,e. â\87§[d, e] T ≡ ↑[d, e] T.
+theorem flift_lift: â\88\80T,d,e. â¬\86[d, e] T ≡ ↑[d, e] T.
-theorem flift_inv_lift: â\88\80d,e,T1,T2. â\87§[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2.
+theorem flift_inv_lift: â\88\80d,e,T1,T2. â¬\86[d, e] T1 ≡ T2 → ↑[d, e] T1 = T2.
-lemma flift_join: â\88\80e1,e2,T. â\87§[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
+lemma flift_join: â\88\80e1,e2,T. â¬\86[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.