+(* Properties with iterated push ********************************************)
+
+lemma isfin_pushs: ān,f. š
ā¦fā¦ ā š
ā¦ā*[n]fā¦.
+#n elim n -n /3 width=3 by isfin_push/
+qed.
+
+(* Inversion lemmas with iterated push **************************************)
+
+lemma isfin_inv_pushs: ān,g. š
ā¦ā*[n]gā¦ ā š
ā¦gā¦.
+#n elim n -n /3 width=3 by isfin_inv_push/
+qed.
+
+(* Properties with tail *****************************************************)
+