proposition: Lemma el_pos x A : x el A -> { n | pos x A = Some n }.
proof: Proof. induction A as [|y A IH]; cbn; intros H. - destruct H as []. - destruct (d x y) as [<-|H1]. + now exists 0. + destruct IH as [n IH]. * destruct H as [->|H]; tauto. * rewrite IH. now exists (S n). Qed.
imports: List Lia Undecidability.PCP.PCP