qed.
(* Inversion lemmas with iterated push **************************************)
lemma isid_inv_pushs: ∀n,g. 𝐈❪⫯*[n]g❫ → 𝐈❪g❫.
qed.
(* Inversion lemmas with iterated push **************************************)
lemma isid_inv_pushs: ∀n,g. 𝐈❪⫯*[n]g❫ → 𝐈❪g❫.