Step
*
of Lemma
mon_ident_q
No Annotations
∀[a:ℚ]. (((a + 0) = a ∈ ℚ) ∧ ((0 + a) = a ∈ ℚ))
BY
{ (ProveSpecializedLemmaWReduce mon_ident) 0 [⌜parm{i}⌝; ⌜<ℚ+>⌝]⋅ }
Latex:
Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  (((a  +  0)  =  a)  \mwedge{}  ((0  +  a)  =  a))
By
Latex:
(ProveSpecializedLemmaWReduce  mon\_ident)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};  \mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}
Home
Index