proposition: Lemma chain_proves_E_rel (h a : nat) (c:chain h) A f : S a <= h -> incl (chain_exists c) A -> A ⊢I rel (findPairLow c (S a)) (findPairHigh c (S a)) (findNum c a) 0 (findNum c (S a)) 0 f -> A ⊢I f.
proof: Proof. intros Ha HA Hpr. eapply IE. 2: eapply Ctx, HA, (@chain_proves_rel _ _ (S a)); lia. unfold rel in Hpr. apply (@chain_proves_P_High h c a). 1-2:lia. 1:easy. apply (@chain_proves_P_Low h c a). 1-2:lia. 1:easy. exact Hpr. 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)