---

Step * of Lemma rel_plus_irreflexive

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;x,y.x R y) ⇒ (∀x:T. (¬(x R+ x))))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN BackThruHyp' 3
   THEN Auto
   THEN D 0
   THEN Auto
   THEN (FLemma `rel_plus_implies` [-1] THENA Auto)
   THEN D -1
   THEN ExRepD) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀[P:T ⟶ ℙ]. ((∀j:T. ((∀k:T. ((k R j) ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T. P[n]})@i'
4. j : T@i
5. ∀k:T. ((k R j) ⇒ (¬(k R+ k)))@i
6. j R+ j@i
7. j R j
⊢ False

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀[P:T ⟶ ℙ]. ((∀j:T. ((∀k:T. ((k R j) ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:T. P[n]})@i'
4. j : T@i
5. ∀k:T. ((k R j) ⇒ (¬(k R+ k)))@i
6. j R+ j@i
7. z : T
8. j R+ z
9. z R j
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (WellFnd\{i\}(T;x,y.x  R  y)  {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}(x  R\msupplus{}  x))))


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  BackThruHyp'  3
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  (FLemma  `rel\_plus\_implies`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index