proposition: Lemma nthe_app_l x n A B : nthe n A = Some x -> nthe n (A ++ B) = Some x.
proof: Proof. revert n. induction A as [|y A IH]; cbn; intros k H. - destruct k; discriminate H. - destruct k as [|k]; cbn in *. exact H. apply IH, H. Qed.
imports: List Lia Undecidability.PCP.PCP