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