proposition: Lemma antiSym (a b : D) : a <<= b -> b <<= a -> a == b.
proof: Proof. Proof using vTrans rho' rho fini decP. intros Ha Hb. destruct (eqDec a b) as [t|Hf]. 1:easy. assert (a << a) as Hc. - eapply leq_less with b. 1:easy. split. 1:easy. intros H. apply Hf. now rewrite H. - exfalso. destruct Hc. firstorder'. 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