n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall
(t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t:
T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n)
n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall
(t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t:
T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n)