proposition: Lemma pos_nth X d (x : X) l n def : pos d x l = Some n -> nth n l def = x.
proof: Proof. revert n; induction l; cbn; intros; try congruence. destruct (d x a); try destruct (pos d x l) eqn:E; inv H; eauto. Qed.
imports: List Lia Undecidability.PCP.PCP