Step
*
of Lemma
param-co-W_wf
∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].  (pco-W ∈ P ⟶ Type)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    (pco-W  \mmember{}  P  {}\mrightarrow{}  Type)
By
Latex:
ProveWfLemma
Home
Index