proposition: Lemma many_argument_appI {P} : head_form P -> exists x As, P = many_argument_app (var x) As /\ Forall (fun A => if A is argument_term Q then normal_form Q else True) As.
proof: Proof. elim. - move=> x. by exists x, []. - move=> {}P Q _ [x] [As] [-> HAs] ?. exists x, (As ++ [argument_term Q]). constructor; first by rewrite many_argument_app_app. rewrite Forall_app. constructor; [done | by constructor]. - move=> {}P t _ [x] [As] [-> HAs]. exists x, (As ++ [argument_poly_type t]). constructor; first by rewrite many_argument_app_app. rewrite Forall_app. constructor; [done | by constructor]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts) ssreflect ssrbool ssrfun