---

Step * of Lemma ancestral-logic-induction

(∀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
{ StartFO }

1
⊢ (∀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)))

---

Latex:


(\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

StartFO

---

Home Index