---

Step * of Lemma list-closed-test_wf

∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T).  (list-closed-test(f;d;L) ∈ {b:𝔹| ↑b ⇐⇒ list-closed(T;L;f)} )
BY
{ ((Auto
    THEN (Subst' list-closed-test(f;d;L) ~ isl(TERMOF{decidable__list-closed2-ext:o, \\v:l, i:l} L f d) 0
          THENA (RW (AddrC [2;1] (TagC (mk_tag_term 4))) 0 THEN Unfold `list-closed-test` 0 THEN Auto)
          )
    )
   THEN (GenConclTerm ⌜TERMOF{decidable__list-closed2-ext:o, \\v:l, i:l} L f d⌝⋅ THENA Auto)
   THEN Thin (-1)) }

1
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)} 

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}f:T  {}\mrightarrow{}  (T  List).  \mforall{}d:EqDecider(T).
        (list-closed-test(f;d;L)  \mmember{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  list-closed(T;L;f)\}  )


By

---

Latex:
((Auto
    THEN  (Subst'  list-closed-test(f;d;L)  \msim{}  isl(TERMOF\{decidable\_\_list-closed2-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  L  f 
                                                                                          d)  0
                THENA  (RW  (AddrC  [2;1]  (TagC  (mk\_tag\_term  4)))  0  THEN  Unfold  `list-closed-test`  0  THEN  Auto)
                )
    )
  THEN  (GenConclTerm  \mkleeneopen{}TERMOF\{decidable\_\_list-closed2-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  L  f  d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index