(* Properties with iterated push ********************************************)
lemma isfin_pushs: ∀n,f. 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
(* Properties with iterated push ********************************************)
lemma isfin_pushs: ∀n,f. 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
qed.
(* Inversion lemmas with iterated push **************************************)
lemma isfin_inv_pushs: ∀n,g. 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
qed.
(* Inversion lemmas with iterated push **************************************)
lemma isfin_inv_pushs: ∀n,g. 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
(* Inversion lemmas with iterated tail **************************************)
lemma isfin_inv_tls: ∀n,f. 𝐅❪⫱*[n]f❫ → 𝐅❪f❫.
(* Inversion lemmas with iterated tail **************************************)
lemma isfin_inv_tls: ∀n,f. 𝐅❪⫱*[n]f❫ → 𝐅❪f❫.