---

Step * of Lemma strongwf-monotone

∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ Type].  (R2 => R1 ⇒ SWellFounded(R1[x;y]) ⇒ SWellFounded(R2[x;y]))
BY
{ ((Auto THEN RepeatFor 5 (ParallelLast)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  Type].    (R2  =>  R1  {}\mRightarrow{}  SWellFounded(R1[x;y])  {}\mRightarrow{}  SWellFounded(R2[x;y]))


By

---

Latex:
((Auto  THEN  RepeatFor  5  (ParallelLast))  THEN  Auto)

---

Home Index