proposition: Lemma pos_length X d (x : X) l n : pos d x l = Some n -> n < | l |.
proof: Proof. revert n; induction l; cbn; intros; try congruence. destruct (d x a). - inv H. lia. - destruct (pos d x l) eqn:E; inv H; try lia. specialize (IHl _ eq_refl). lia. Qed.
imports: List Lia Undecidability.PCP.PCP