Step
*
of Lemma
atom-sdata_wf
∀[a:Atom1]. (data(a) ∈ SecurityData)
BY
{ (Unfold `sdata` 0 THEN ProveWfLemma) }
Latex:
Latex:
\mforall{}[a:Atom1].  (data(a)  \mmember{}  SecurityData)
By
Latex:
(Unfold  `sdata`  0  THEN  ProveWfLemma)
Home
Index