Step * of Lemma Msg_sub_wf

[M:IdLnk ─→ Id ─→ Type]. ∀[l:IdLnk].  (Msg_sub(l;M) ∈ Type)
BY
(Unfold `Msg_sub` THEN Auto) }


Latex:


\mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[l:IdLnk].    (Msg\_sub(l;M)  \mmember{}  Type)


By

(Unfold  `Msg\_sub`  0  THEN  Auto)




Home Index