---

Step * 2 of Lemma assert_of_eq_atom1


1. x : Atom1
2. y : Atom1
3. x = y ∈ Atom1
⊢ ↑x =a1 y
BY
{ (Subst' x =a1 y ~ tt 0 THEN Reduce 0 THEN Try (Trivial)) }

1
.....equality..... 
1. x : Atom1
2. y : Atom1
3. x = y ∈ Atom1
⊢ x =a1 y ~ tt

---

Latex:

---

Latex:

1.  x  :  Atom1
2.  y  :  Atom1
3.  x  =  y
\mvdash{}  \muparrow{}x  =a1  y


By

---

Latex:
(Subst'  x  =a1  y  \msim{}  tt  0  THEN  Reduce  0  THEN  Try  (Trivial))

---

Home Index