proposition: Lemma nthe_length A n : length A > n -> { x | nthe n A = Some x }.
proof: Proof. revert n. induction A as [|y A IH]; cbn; intros n H. - exfalso. lia. - destruct n as [|n]; cbn. + now exists y. + destruct (IH n) as [x H1]. lia. now exists x. Qed.
imports: List Lia Undecidability.PCP.PCP