---

Step * of Lemma atom-sdata-one-one

∀[a,b:Atom1].  uiff(data(a) = data(b) ∈ SecurityData;a = b ∈ Atom1)
BY
{ Auto }

1
1. a : Atom1
2. b : Atom1
3. data(a) = data(b) ∈ SecurityData
⊢ a = b ∈ Atom1

---

Latex:

---

Latex:
\mforall{}[a,b:Atom1].    uiff(data(a)  =  data(b);a  =  b)


By

---

Latex:
Auto

---

Home Index