Step
*
of Lemma
xxsym_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. (sym(T;E) ∈ ℙ)
BY
{ ((Unfold `xxsym` 0) THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[E:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}]. (sym(T;E) \mmember{} \mBbbP{})
By
Latex:
((Unfold `xxsym` 0) THEN Auto)
Home
Index