---

Step * of Lemma atom2-deq_wf

Atom2Deq ∈ EqDecider(Atom2)
BY
{ (Unfold `deq` 0
   THEN ProveWfLemma
   THEN InstLemma `atom2-deq-aux` []
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN (BHyp 1 THEN Auto)⋅) }

---

Latex:

---

Latex:
Atom2Deq  \mmember{}  EqDecider(Atom2)


By

---

Latex:
(Unfold  `deq`  0
  THEN  ProveWfLemma
  THEN  InstLemma  `atom2-deq-aux`  []
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  (BHyp  1  THEN  Auto)\mcdot{})

---

Home Index