---

Step * of Lemma wellfounded-anti-reflexive

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀[a:T]. (¬R[a;a]) supposing WellFnd{i}(T;x,y.R[x;y])
BY
{ (Auto THEN (WFndHypInd (-2) (-1)) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (WFndHypInd  (-2)  (-1))  THEN  Auto)

---

Home Index