---

Step * of Lemma Wless_antireflexive

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[w1:W(A;a.B[a])].  (¬(w1 <  w1))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN UseWInductionLemma
   THEN RepeatFor 2 (RecUnfold `Wcmp` 0)
   THEN Reduce 0
   THEN RepUR ``Wsup`` 0) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A@i
4. f : B[a] ⟶ W(A;a.B[a])@i
5. ∀b:B[a]. (¬((f b) <  (f b)))@i
⊢ ¬(∃x:B[a]. ∀x@0:B[a]. ((f x@0) <  (f x)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w1:W(A;a.B[a])].    (\mneg{}(w1  <    w1))


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  UseWInductionLemma
  THEN  RepeatFor  2  (RecUnfold  `Wcmp`  0)
  THEN  Reduce  0
  THEN  RepUR  ``Wsup``  0)

---

Home Index