-lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≗ f.
-/3 width=6 by isid_after_dx, after_mono/
-qed-.
+lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈⦃f1⦄ → f2 ≡ f.
+/3 width=6 by after_isid_sn, after_mono/ qed-.
+
+lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈⦃f2⦄ → f1 ≡ f.
+/3 width=6 by after_isid_dx, after_mono/ qed-.