---

Step * of Lemma ses-private-one-one

∀[s:SES]. ∀[A,B:Id].  uiff(PrivateKey(A) = PrivateKey(B) ∈ Key;A = B ∈ Id) supposing PropertyK
BY
{ (Unfolds``encryption-key ses-private-key`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[A,B:Id].    uiff(PrivateKey(A)  =  PrivateKey(B);A  =  B)  supposing  PropertyK


By

---

Latex:
(Unfolds``encryption-key  ses-private-key``  0  THEN  Auto)

---

Home Index