---

Step * of Lemma id-sdata-one-one

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index