(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T1] â\86\92 ð\9d\95\8a[T2].
+lemma lifts_simple_dx: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T1] â\86\92 ð\9d\90\92[T2].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\95\8a[T2] â\86\92 ð\9d\95\8a[T1].
+lemma lifts_simple_sn: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 ð\9d\90\92[T2] â\86\92 ð\9d\90\92[T1].
#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
qed-.