Step
*
of Lemma
int-minus-comparison_wf
∀[T:Type]. ∀[f:T ⟶ ℤ].  (int-minus-comparison(f) ∈ comparison(T))
BY
{ (Auto THEN RepUR ``int-minus-comparison comparison`` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto') }
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (int-minus-comparison(f)  \mmember{}  comparison(T))
By
Latex:
(Auto  THEN  RepUR  ``int-minus-comparison  comparison``  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto')
Home
Index