Step
*
of Lemma
CLK_headers_fun_wf
∀[MsgType:ValueAllType]. (CLK_headers_fun(MsgType) ∈ Name ─→ Type)
BY
{ ProveEmlWfLemma }
Latex:
Latex:
\mforall{}[MsgType:ValueAllType].  (CLK\_headers\_fun(MsgType)  \mmember{}  Name  {}\mrightarrow{}  Type)
By
Latex:
ProveEmlWfLemma
Home
Index