Step
*
of Lemma
itermMinus_wf
∀[num:int_term()]. ("-"num ∈ int_term())
BY
{ DepprodCoDatatypeConstructorWf `int_term_size` }
Latex:
Latex:
\mforall{}[num:int\_term()].  ("-"num  \mmember{}  int\_term())
By
Latex:
DepprodCoDatatypeConstructorWf  `int\_term\_size`
Home
Index