---

Step * of Lemma rv-add-assoc

∀[rv:RealVectorSpace]. ∀[x,y,z:Point].  x + y + z ≡ x + y + z
BY
{ (Auto
   THEN (D 1 THENA Auto)
   THEN Unfold `rv-add` 0
   THEN OnMaybeHyp 9 (\h. (MemTypeHD h
                           THEN ∀h:hyp. Fold `member` h 
                           THEN Try (MemCD)
                           THEN (Unhide THENM (ExRepD THEN BackThruSomeHyp))
                           THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[x,y,z:Point].    x  +  y  +  z  \mequiv{}  x  +  y  +  z


By

---

Latex:
(Auto
  THEN  (D  1  THENA  Auto)
  THEN  Unfold  `rv-add`  0
  THEN  OnMaybeHyp  9  (\mbackslash{}h.  (MemTypeHD  h
                                                  THEN  \mforall{}h:hyp.  Fold  `member`  h 
                                                  THEN  Try  (MemCD)
                                                  THEN  (Unhide  THENM  (ExRepD  THEN  BackThruSomeHyp))
                                                  THEN  Auto)))

---

Home Index