---

Step * of Lemma qv-add_wf

∀[as,bs:ℚ List].  qv-add(as;bs) ∈ ℚ List supposing dimension(as) = dimension(bs) ∈ ℤ
BY
{ (Unfold `qv-dim` 0
   THEN InductionOnList
   THEN RecUnfold `qv-add` 0
   THEN Reduce 0
   THEN Auto'
   THEN BackThruSomeHyp
   THEN DVar `bs'
   THEN All Reduce
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbQ{}  List].    qv-add(as;bs)  \mmember{}  \mBbbQ{}  List  supposing  dimension(as)  =  dimension(bs)


By

---

Latex:
(Unfold  `qv-dim`  0
  THEN  InductionOnList
  THEN  RecUnfold  `qv-add`  0
  THEN  Reduce  0
  THEN  Auto'
  THEN  BackThruSomeHyp
  THEN  DVar  `bs'
  THEN  All  Reduce
  THEN  Auto')

---

Home Index