∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y) 
 TC(λa,b.P a b)(x,y))
{ StartFO }
⊢ ∀x,y:Dom.  (TC(λa,b.TC(λi,j.P i j)(a,b))(x,y)