---

Step * of Lemma Wleq-Wadd

∀[A:Type]. ∀[B:A ⟶ Type].  ∀zero:A ⟶ 𝔹. ∀w3,w2,w1:W(A;a.B[a]).  ((w1 ≤  w2) ⇒ ((w1 + w3) ≤  (w2 + w3)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN UseWInductionLemma
   THEN Auto
   THEN RecUnfold `Wadd` 0
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN Fold `Wsup` 0
   THEN AutoSplit
   THEN MoveToConcl (-2)
   THEN RepeatFor 2 ((ReduceWcmp 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}zero:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}w3,w2,w1:W(A;a.B[a]).    ((w1  \mleq{}    w2)  {}\mRightarrow{}  ((w1  +  w3)  \mleq{}    (w2  +  w3)))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  RecUnfold  `Wadd`  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit
  THEN  MoveToConcl  (-2)
  THEN  RepeatFor  2  ((ReduceWcmp  0  THEN  Auto)))

---

Home Index