---

Step * 1 of Lemma atom2-deq-aux


1. a : Atom2
2. b : Atom2
3. ↑a =a2 b
⊢ a = b ∈ Atom2
BY
{ (RW assert_pushdownC (-1)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  Atom2
2.  b  :  Atom2
3.  \muparrow{}a  =a2  b
\mvdash{}  a  =  b


By

---

Latex:
(RW  assert\_pushdownC  (-1)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index