(* Forward lemmas with weight for binders ***********************************)
-lemma liftsb_fwd_bw: â\88\80f,I1,I2. â¬\86*[f] I1 ≘ I2 → ♯{I1} = ♯{I2}.
+lemma liftsb_fwd_bw: â\88\80f,I1,I2. â\87§*[f] I1 ≘ I2 → ♯{I1} = ♯{I2}.
#f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/
qed-.