---

Step * 1 1 of Lemma norm-list_wf


1. T : Type
2. value-type(T)
3. N : id-fun(T)
4. u : T
5. v : T List
6. norm-list(N) v ∈ {y:T List| v = y ∈ (T List)} 
⊢ [u / v] = [N u / (norm-list(N) v)] ∈ (T List)
BY
{ (EqCD THEN Auto THEN (GenConclAtAddr [3] THEN D -2 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  N  :  id-fun(T)
4.  u  :  T
5.  v  :  T  List
6.  norm-list(N)  v  \mmember{}  \{y:T  List|  v  =  y\} 
\mvdash{}  [u  /  v]  =  [N  u  /  (norm-list(N)  v)]


By

---

Latex:
(EqCD  THEN  Auto  THEN  (GenConclAtAddr  [3]  THEN  D  -2  THEN  Auto)\mcdot{})

---

Home Index