-lemma pred_inv_appl: â\88\80M,N. M ⥤ N → ∀B,A. @B.A = M →
- (â\88\83â\88\83D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨
- â\88\83â\88\83A0,D,C0. B ⥤ D & A0 ⥤ C0 & ð\9d\9b\8c.A0 = A & [â¬\90D]C0 = N.
+lemma pred_inv_appl: â\88\80M,N. M â¤\87 N → ∀B,A. @B.A = M →
+ (â\88\83â\88\83D,C. B â¤\87 D & A â¤\87 C & @D.C = N) ∨
+ â\88\83â\88\83A0,D,C0. B â¤\87 D & A0 â¤\87 C0 & ð\9d\9b\8c.A0 = A & [â\86\99D]C0 = N.