---

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