---

Step * 1 of Lemma list-closed-test_wf


1. T : Type
2. L : T List
3. f : T ⟶ (T List)
4. d : EqDecider(T)
5. v : Dec(list-closed(T;L;f))
⊢ isl(v) ∈ {b:𝔹| ↑b ⇐⇒ list-closed(T;L;f)} 
BY
{ ((D -1 THEN Reduce 0) THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  f  :  T  {}\mrightarrow{}  (T  List)
4.  d  :  EqDecider(T)
5.  v  :  Dec(list-closed(T;L;f))
\mvdash{}  isl(v)  \mmember{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  list-closed(T;L;f)\} 


By

---

Latex:
((D  -1  THEN  Reduce  0)  THEN  MemTypeCD  THEN  Auto)

---

Home Index