---

Step * of Lemma eq_atom_eq_true_elim

∀[x,y:Atom].  x = y ∈ Atom supposing x =a y = tt
BY
{ Auto }

1
1. x : Atom
2. y : Atom
3. x =a y = tt
⊢ x = y ∈ Atom

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].    x  =  y  supposing  x  =a  y  =  tt


By

---

Latex:
Auto

---

Home Index