---

Step * 1 of Lemma deq-fset_wf

.....equality..... 
1. T : Type
2. eq : EqDecider(T)
⊢ TERMOF{decidable__equal_fset:o, 1:l, 1:l} ~ TERMOF{decidable__equal_fset:o, \\v:l, i:l}
BY
{ SqequalBySymbComp200 }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  TERMOF\{decidable\_\_equal\_fset:o,  1:l,  1:l\}  \msim{}  TERMOF\{decidable\_\_equal\_fset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}


By

---

Latex:
SqequalBySymbComp200

---

Home Index