---

Step * 1 of Lemma awf-solution_wf

.....equality..... 
1. A : Type
2. I : Type
3. G : awf-system{i:l}(I;A)@i'
⊢ awf-solution(G) ~ TERMOF{unique-awf:o, i:l, i:l} G
BY
{ (RW (BasicSymbolicComputeC []) 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  Type
2.  I  :  Type
3.  G  :  awf-system\{i:l\}(I;A)@i'
\mvdash{}  awf-solution(G)  \msim{}  TERMOF\{unique-awf:o,  i:l,  i:l\}  G


By

---

Latex:
(RW  (BasicSymbolicComputeC  [])  0  THEN  Auto)

---

Home Index