---

Step * of Lemma TC-ind

∀[Dom:Type]. ∀[B:Dom ─→ ℙ]. ∀[R:Dom ─→ Dom ─→ ℙ].
  ((∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))) ⇒ (∀x,y:Dom.  (TC(λa,b.R a b)(x,y) ⇒ (B x) ⇒ (B y))))
BY
{ Auto }

1
1. [Dom] : Type
2. [B] : Dom ─→ ℙ
3. [R] : Dom ─→ Dom ─→ ℙ
4. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
5. x : Dom@i
6. y : Dom@i
7. TC(λa,b.R a b)(x,y)@i
8. B x@i
⊢ B y

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[B:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y)))  {}\mRightarrow{}  (\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.R  a  b)(x,y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))))


By

Auto

---

Home Index