Step
*
of Lemma
sdata-pair?_wf
∀[p:SecurityData]. (sdata-pair?(p) ∈ 𝔹)
BY
{ (Unfold `sdata` 0 THEN ProveWfLemma) }
Latex:
Latex:
\mforall{}[p:SecurityData]. (sdata-pair?(p) \mmember{} \mBbbB{})
By
Latex:
(Unfold `sdata` 0 THEN ProveWfLemma)
Home
Index