proposition: Lemma find_Some x A n: find x A = Some n -> nth A n = Some x.
proof: Proof. induction A in n |-*; cbn. - discriminate. - destruct (x == a). injection 1; intros; subst. reflexivity. destruct find; try discriminate. cbn; injection 1; intros; subst. cbn. now rewrite IHA. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)