---

Step * 1 2 of Lemma sdata-pair-free-from-atom

.....subterm..... T:t
2:n
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ Ax ∈ b#<d1, d2>:SecurityData supposing b#d1:SecurityData ∧ b#d2:SecurityData
BY
{ Unfold `uimplies` 0 }

1
1. b : Atom1
2. d1 : SecurityData
3. d2 : SecurityData
⊢ Ax ∈ ∩:b#d1:SecurityData ∧ b#d2:SecurityData. b#<d1, d2>:SecurityData

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  b  :  Atom1
2.  d1  :  SecurityData
3.  d2  :  SecurityData
\mvdash{}  Ax  \mmember{}  b\#<d1,  d2>:SecurityData  supposing  b\#d1:SecurityData  \mwedge{}  b\#d2:SecurityData


By

---

Latex:
Unfold  `uimplies`  0

---

Home Index