---

Step * 1 2 1 of Lemma enum-fin-seq-max2_wf


1. M : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (ℕ?)
2. m : ℕ
⊢ (λx.tt ∈ enum-fin-seq(m))
BY
{ ((InstLemma `enum-fin-seq-true` [⌜m⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  (\mBbbN{}?)
2.  m  :  \mBbbN{}
\mvdash{}  (\mlambda{}x.tt  \mmember{}  enum-fin-seq(m))


By

---

Latex:
((InstLemma  `enum-fin-seq-true`  [\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index