(* Specific inversion lemmas ************************************************)
-lemma isid_inv_seq: â\88\80f,n. ð\9d\90\88â¦\83n⨮fâ¦\84 â\86\92 ð\9d\90\88â¦\83fâ¦\84 ∧ 0 = n.
+lemma isid_inv_seq: â\88\80f,n. ð\9d\90\88â\9dªn⨮fâ\9d« â\86\92 ð\9d\90\88â\9dªfâ\9d« ∧ 0 = n.
#f #n #H elim (isid_inv_gen … H) -H
#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
qed-.