proposition: Fact head_form_ren_term {ζ ξ P} : head_form P -> head_form (ren_term ζ ξ P).
proof: Proof. move=> H. move: P H ζ ξ. apply: (head_form_ind' (fun P _ => forall ζ ξ, normal_form (ren_term ζ ξ P)) (fun P _ => forall ζ ξ, head_form (ren_term ζ ξ P))); by eauto using normal_form, head_form. 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