proposition: Lemma safe_poly_typeP {n ss x} : is_safe_poly_type 0 (safe_poly_type n ss x).
proof: Proof. have ->: x = 0 + x by lia. move: (0) => k. elim: n k. - move=> k. elim: ss; [move=> /=; by lia | by move=> /= ? [|? ?]]. - move=> n IH k /=. have ->: S (n + (k + x)) = n + ((S k) + x) by lia. by apply: IH. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun