---

Step * 1 of Lemma atom-sdata-one-one


1. a : Atom1
2. b : Atom1
3. data(a) = data(b) ∈ SecurityData
⊢ a = b ∈ Atom1
BY
{ RepUR ``atom-sdata sdata`` (-1) }

1
1. a : Atom1
2. b : Atom1
3. tree_leaf(inr a ) = tree_leaf(inr b ) ∈ tree(Id + Atom1)
⊢ a = b ∈ Atom1

---

Latex:

---

Latex:

1.  a  :  Atom1
2.  b  :  Atom1
3.  data(a)  =  data(b)
\mvdash{}  a  =  b


By

---

Latex:
RepUR  ``atom-sdata  sdata``  (-1)

---

Home Index