---

Step * 1 1 2 1 3 4 1 1 1 1 1 1 1 2 1 1 2 2 2 1 1 1 of Lemma partition-refinement-sum


∀p,q,r:ℝ List. ∀x1:ℝ. ∀i:ℕ||q @ [x1 / r]||.  ((p = (q @ [x1 / r]) ∈ (ℝ List)) ⇒ (q @ [x1 / r][i] = p[i]))
BY
{ TACTIC:(Auto THEN BLemma `req_weakening` THEN Auto THEN Try ((EqCD THEN Auto)) THEN HypSubst'  (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

\mforall{}p,q,r:\mBbbR{}  List.  \mforall{}x1:\mBbbR{}.  \mforall{}i:\mBbbN{}||q  @  [x1  /  r]||.    ((p  =  (q  @  [x1  /  r]))  {}\mRightarrow{}  (q  @  [x1  /  r][i]  =  p[i]))


By

---

Latex:
TACTIC:(Auto
                THEN  BLemma  `req\_weakening`
                THEN  Auto
                THEN  Try  ((EqCD  THEN  Auto))
                THEN  HypSubst'    (-1)  0
                THEN  Auto)

---

Home Index