---

Step * of Lemma Wleq_weakening2

∀[A:Type]. ∀[B:A ⟶ Type].  ∀w1,w2:W(A;a.B[a]).  w1 ≤  w2 supposing w1 = w2 ∈ W(A;a.B[a])
BY
{ (Auto THEN RevHypSubst' (-1) 0 THEN Auto THEN RepeatFor 2 (Thin (-1)) THEN MoveToConcl (-1) THEN UseWInductionLemma) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W(A;a.B[a])
5. ∀b:B[a]. ((f b) ≤  (f b))
⊢ Wsup(a;f) ≤  Wsup(a;f)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    \mforall{}w1,w2:W(A;a.B[a]).    w1  \mleq{}    w2  supposing  w1  =  w2


By

---

Latex:
(Auto
  THEN  RevHypSubst'  (-1)  0
  THEN  Auto
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  MoveToConcl  (-1)
  THEN  UseWInductionLemma)

---

Home Index