(* Properties with basic relocation *****************************************)
-lemma lifts_lref_lt (m,n,i): i < m â\86\92 â¬\86[m,n] #i ≘ #i.
+lemma lifts_lref_lt (m,n,i): i < m â\86\92 â\87§[m,n] #i ≘ #i.
/3 width=1 by lifts_lref, at_basic_lt/ qed.
-lemma lifts_lref_ge (m,n,i): m â\89¤ i â\86\92 â¬\86[m,n] #i ≘ #(n+i).
+lemma lifts_lref_ge (m,n,i): m â\89¤ i â\86\92 â\87§[m,n] #i ≘ #(n+i).
/3 width=1 by lifts_lref, at_basic_ge/ qed.
-lemma lifts_lref_ge_minus (m,n,i): n+m â\89¤ i â\86\92 â¬\86[m,n] #(i-n) ≘ #i.
+lemma lifts_lref_ge_minus (m,n,i): n+m â\89¤ i â\86\92 â\87§[m,n] #(i-n) ≘ #i.
#m #n #i #Hi
>(plus_minus_m_m i n) in ⊢ (???%);
/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/