proposition: Lemma δP : Forall (fun c => match c with | (h10c_one x) => x < δ | (h10c_plus x y z) => x < δ /\ y < δ /\ z < δ | (h10c_mult x y z) => x < δ /\ y < δ /\ z < δ end) h10cs.
proof: Proof. rewrite /δ. elim: (h10cs); first by constructor. move=> c cs IH. constructor. - case: c => /= *; by lia. - apply: Forall_impl IH. move: c => + []; case => > /=; by lia. 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