---

Step * of Lemma atom-sdata-has-atom

∀[a,b:Atom1].  uiff(b#data(a):SecurityData;¬(a = b ∈ Atom1))
BY
{ At ⌜Type⌝ Auto⋅ }

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

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

---

Latex:

---

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


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  Auto\mcdot{}

---

Home Index