Step
*
of Lemma
Spread_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  (Spread(Pos;a.Mv[a]) ∈ Type)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[Pos:Type].  \mforall{}[Mv:Pos  {}\mrightarrow{}  Type].    (Spread(Pos;a.Mv[a])  \mmember{}  Type)
By
Latex:
ProveWfLemma
Home
Index