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