---

Step * of Lemma mon_assoc_q

No Annotations
∀[a,b,c:ℚ].  ((a + b + c) = ((a + b) + c) ∈ ℚ)
BY
{ (ProveSpecializedLemmaWReduce mon_assoc) 0 [⌜parm{i}⌝; ⌜<ℚ+>⌝]⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b,c:\mBbbQ{}].    ((a  +  b  +  c)  =  ((a  +  b)  +  c))


By

---

Latex:
(ProveSpecializedLemmaWReduce  mon\_assoc)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};  \mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}

---

Home Index