(* Forward lemmas with weight for binders ***********************************)
-lemma liftsb_fwd_bw: â\88\80f,I1,I2. â¬\86*[f] I1 â\89\98 I2 â\86\92 â\99¯{I1} = â\99¯{I2}.
+lemma liftsb_fwd_bw: â\88\80f,I1,I2. â\87§*[f] I1 â\89\98 I2 â\86\92 â\99¯â\9d¨I1â\9d© = â\99¯â\9d¨I2â\9d©.
#f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/
qed-.