proposition: Lemma ksatisTransport : (~ H10UPC_SAT h10) -> ksatis ((F (ff:=falsity_on) (h10:=h10)) → falsity).
proof: Proof. intros H. exists dom. pose (kripke_tarski (ff:=falsity_on) (IB (h10:=h10))) as Hk. exists (interp_kripke (IB (h10:=h10))). exists tt. exists (fun _ => Num 0). rewrite <- Hk. intros HF. apply H. eapply IB_fulfills. easy. 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)