proposition: Lemma pairlist_dec X Y (L : list (X * Y)) y : eq_dec X -> eq_dec Y -> dec (exists x, (x, y) el L).
proof: Proof. intros DX DY. induction L as [|[a b]]. - right. firstorder. - destruct IHL as [H|H]. + left. destruct H as [x Hx]. exists x. now right. + decide (y = b) as [->|Hy]. * left. exists a. now left. * right. intros [x[Hx|Hx]]. -- apply Hy. congruence. -- apply H. now exists x. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List