---

Step * of Lemma secret-table_wf

∀[T:Id ─→ Type]. (secret-table(T) ∈ Type)
BY
{ (Unfold `secret-table` 0 THEN Auto) }

---

Latex:


\mforall{}[T:Id  {}\mrightarrow{}  Type].  (secret-table(T)  \mmember{}  Type)


By

(Unfold  `secret-table`  0  THEN  Auto)

---

Home Index