proposition: Lemma find_in x A: x ∈ A -> exists n, find x A = Some n.
proof: Proof. induction A; cbn; intuition idtac. - exists 0. destruct (x == a); subst; intuition easy. - destruct (x == a). + subst; exists 0; intuition easy. + destruct H as [m]; exists (S m); intuition idtac. rewrite H; reflexivity. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)