Step
*
of Lemma
utrans_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. (UniformlyTrans(T;x,y.E[x;y]) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[E:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. (UniformlyTrans(T;x,y.E[x;y]) \mmember{} \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index