English
Assume that whenever sel(s) = some a, then a ∈ s. Then if Enumerate(sel)(s,n) = some a, we must have a ∈ s.
Русский
Пусть при sel(s) = some a следует, что a ∈ s. Тогда если Enumerate(sel)(s,n) = some a, то a ∈ s.
LaTeX
$$$\Big(\forall s,a,\ sel(s) = \mathrm{some} a \Rightarrow a \in s\Big) \Rightarrow \forall s,n,a,\ \operatorname{Enumerate}_{sel}(s,n) = \mathrm{some} a \Rightarrow a \in s$$$
Lean4
theorem enumerate_mem (h_sel : ∀ s a, sel s = some a → a ∈ s) : ∀ {s n a}, enumerate sel s n = some a → a ∈ s
| s, 0, a => h_sel s a
| s, n + 1, a => by
cases h : sel s with
| none => simp [enumerate_eq_none_of_sel, h]
| some a' =>
simp only [enumerate, h]
exact fun h' : enumerate sel (s \ { a' }) n = some a ↦
have : a ∈ s \ { a' } := enumerate_mem h_sel h'
this.left
