(* Specific forward lemmas **************************************************)
lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.
(* Specific forward lemmas **************************************************)
lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.