-lemma nta_ldef_drops (a) (h) (G) (K) (L) (i):
- â\88\80V,W. â¦\83G,Kâ¦\84 â\8a¢ V :[a,h] W →
- â\88\80U. â¬\86*[â\86\91i] W â\89\98 U â\86\92 â¬\87*[i] L â\89\98 K.â\93\93V â\86\92 â¦\83G,Lâ¦\84 â\8a¢ #i :[a,h] U.
-#a #h #G #K #L #i #V #W #HVW #U #HWU #HLK
-elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d´1â\9dµ) (ð\9d\90\94â\9d´iâ\9dµ)) [| // ] #X #HWX #HXU
+lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
+ â\88\80V,W. â\9dªG,Kâ\9d« â\8a¢ V :[h,a] W →
+ â\88\80U. â\87§[â\86\91i] W â\89\98 U â\86\92 â\87©[i] L â\89\98 K.â\93\93V â\86\92 â\9dªG,Lâ\9d« â\8a¢ #i :[h,a] U.
+#h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
+elim (lifts_split_trans â\80¦ HWU (ð\9d\90\94â\9d¨1â\9d©) (ð\9d\90\94â\9d¨iâ\9d©)) [| // ] #X #HWX #HXU