---

Step * 1 1 of Lemma ancestral-logic-example2

.....assertion..... 
⊢ ∀x,y:Dom.  (TC(λa,b.P a b)(x,y) ⇒ TC(λa,b.P a b)(x,y))
BY
{ (RepeatFor 2 (FOAllIntro) THEN FOImpliesIntro THEN FOHyp (-1)) }

---

Latex:


.....assertion..... 
\mvdash{}  \mforall{}x,y:Dom.    (TC(\mlambda{}a,b.P  a  b)(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))


By

(RepeatFor  2  (FOAllIntro)  THEN  FOImpliesIntro  THEN  FOHyp  (-1))

---

Home Index