proposition: Lemma erel_findNum_ExI (a b c d h : nat) (cc:chain h) A : (forall pl pr, (erel_findNum_H a b c d pl pr cc ++ A) ⊢I wFalse 1) -> A ⊢I erel_findNum a b c d cc .
proof: Proof. intros Hpr. unfold erel_findNum, erel_i. doAllI pr. cbn [subst_form]. doAllI pl. cbn. do 11 apply II. eapply Weak. 1: apply (Hpr pl pr). apply incl_app. - unfold erel_findNum_H. now repeat apply cons_incl_proper. - now do 11 apply incl_tl. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)