Step
*
of Lemma
ancestral-logic-example2
∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) 
⇒ TC(λa,b.P a b)(x,y))
BY
{ StartFO }
1
⊢ ∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) 
⇒ TC(λa,b.P a b)(x,y))
Latex:
Latex:
\mforall{}x,y:Dom.    (TC(\mlambda{}a,b.TC(\mlambda{}i,j.P  i  j)(a,b))(x,y)  {}\mRightarrow{}  TC(\mlambda{}a,b.P  a  b)(x,y))
By
Latex:
StartFO
Home
Index