---

Step * 1 1 of Lemma norm-list_wf_sq


1. T : Type
2. T ⊆r Base
3. value-type(T)
4. N : sq-id-fun(T)
5. SQType(T List)
6. SQType(T)
7. u : T
8. v : T List
9. norm-list(N) v ∈ {y:T List| v ~ y} 
10. value-type(T List)
⊢ [u / v] = [N u / (norm-list(N) v)] ∈ (T List)
BY
{ (EqCD THEN Auto THEN (GenConclAtAddr [3] THEN D -2 THEN Auto THEN HypSubst' -2 0 THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  value-type(T)
4.  N  :  sq-id-fun(T)
5.  SQType(T  List)
6.  SQType(T)
7.  u  :  T
8.  v  :  T  List
9.  norm-list(N)  v  \mmember{}  \{y:T  List|  v  \msim{}  y\} 
10.  value-type(T  List)
\mvdash{}  [u  /  v]  =  [N  u  /  (norm-list(N)  v)]


By

---

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

---

Home Index