---

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


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index