---

Step * of Lemma norm-list_wf

∀[T:Type]. ∀[N:id-fun(T)]. (norm-list(N) ∈ id-fun(T List)) supposing value-type(T)
BY
{ (Auto THEN Unfold `id-fun` 0 THEN ExtWith [`L'] [⌜Top ⟶ Top⌝]⋅ THEN Auto THEN Try (ProveWfLemma)) }

1
1. T : Type
2. value-type(T)
3. N : id-fun(T)
4. L : T List
⊢ norm-list(N) L ∈ {y:T List| L = y ∈ (T List)} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[N:id-fun(T)].  (norm-list(N)  \mmember{}  id-fun(T  List))  supposing  value-type(T)


By

---

Latex:
(Auto  THEN  Unfold  `id-fun`  0  THEN  ExtWith  [`L']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Try  (ProveWfLemma))

---

Home Index