proposition: Lemma helper_iP (a b c a' b' c':D) : iP a b c -> a==a'->b==b'->c==c' -> iP a' b' c'.
proof: Proof. intros [Hpa [Hnb [Hnc [Hpl Hpr]]]] Ha Hb Hc. cbn in Hpa,Hnb,Hnc,Hpl,Hpr. split. 2:split. 3:split. 4:split. - intros Hcc. apply Hpa. cbn in Hcc. now rewrite Ha. - now rewrite <- Hb. - now rewrite <- Hc. - now apply (rewrite_iPr Hpl). - now apply (rewrite_iPr Hpr). Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions