#f #g #Hf #Hg @(eq_push ā¦ Hg) [2: @eq_push_inv_isid // | skip ]
@eq_f //
qed-.
+
+(* Properties with iterated push ********************************************)
+
+lemma isid_pushs: ān,f. šā¦fā¦ ā šā¦ā*[n]fā¦.
+#n elim n -n /3 width=3 by isid_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isid_inv_pushs: ān,g. šā¦ā*[n]gā¦ ā šā¦gā¦.
+#n elim n -n /3 width=3 by isid_inv_push/
+qed.
+
+(* Properties with tail *****************************************************)
+
+lemma isid_tl: āf. šā¦fā¦ ā šā¦ā«±fā¦.
+#f cases (pn_split f) * #g * -f #H
+[ /2 width=3 by isid_inv_push/
+| elim (isid_inv_next ā¦ H) -H //
+]
+qed.
+
+(* Properties with iterated tail ********************************************)
+
+lemma isid_tls: ān,g. šā¦gā¦ ā šā¦ā«±*[n]gā¦.
+#n elim n -n /3 width=1 by isid_tl/
+qed.