DEFINITION node_inh()
TYPE =
       ∀g:G.∀n:nat.∀k:nat.(ex_2 C T λc:C.λt:T.arity g c t (ASort k n))
BODY =
Show proof