---

Step * of Lemma assert_of_eq_atom

∀[x,y:Atom].  uiff(↑x =a y;x = y ∈ Atom)
BY
{ ((OnConcl (Unfold_o eq_atom) THEN GenUnivCD) THENA Auto) }

1
1. x : Atom
2. y : Atom
3. ↑if x=y then tt else ff fi 
⊢ x = y ∈ Atom

2
1. x : Atom
2. y : Atom
3. x = y ∈ Atom
⊢ ↑if x=y then tt else ff fi 

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].    uiff(\muparrow{}x  =a  y;x  =  y)


By

---

Latex:
((OnConcl  (Unfold\_o  eq\_atom)  THEN  GenUnivCD)  THENA  Auto)

---

Home Index