proposition: Lemma normal_form_many_app {P Qs} : normal_form (many_app P Qs) -> normal_form P /\ Forall normal_form Qs.
proof: Proof. elim /rev_ind: Qs P; first by (move=> *; constructor). move=> Q Qs IH P. rewrite many_app_app /=. move H1P': (app _ _) => P' H2P'. case: H2P' H1P'; [|done|done]. move=> ? []; [done| |done]. move=> ? ? /normal_form_head_form + + [? ?]. subst. move=> /IH [? ?] ?. constructor; first done. apply /Forall_app. constructor; first 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