---

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


1. x1 : SecurityData
2. x2 : SecurityData
3. y1 : SecurityData
4. y2 : SecurityData
5. <x1, x2> = <y1, y2> ∈ SecurityData
⊢ x1 = y1 ∈ SecurityData
BY
{ (ApFunToHypEquands `Z' ⌈if sdata-pair?(Z) then sdata-left(Z) else x1 fi ⌉ ⌈SecurityData⌉ (-1)⋅
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  x1  :  SecurityData
2.  x2  :  SecurityData
3.  y1  :  SecurityData
4.  y2  :  SecurityData
5.  <x1,  x2>  =  <y1,  y2>
\mvdash{}  x1  =  y1


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}if  sdata-pair?(Z)  then  sdata-left(Z)  else  x1  fi  \mkleeneclose{}  \mkleeneopen{}SecurityData\mkleeneclose{}  (-1)\mcdot{}
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index