---

Step * of Lemma Spread-family_wf

∀[P,Pos:Type]. ∀[f:Pos ⟶ ℤ]. ∀[Mv:p:ℤ ⟶ P ⟶ P ⟶ Type].  (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q]) ∈ P ⟶ Type)
BY
{ ProveWfLemma⋅ }

---

Latex:

---

Latex:
\mforall{}[P,Pos:Type].  \mforall{}[f:Pos  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[Mv:p:\mBbbZ{}  {}\mrightarrow{}  P  {}\mrightarrow{}  P  {}\mrightarrow{}  Type].
    (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q])  \mmember{}  P  {}\mrightarrow{}  Type)


By

---

Latex:
ProveWfLemma\mcdot{}

---

Home Index