T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
(TSort n) H5) in (False_ind P H6)))))))))))))) i v y x H0))) H)))))).
T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I
(TSort n) H5) in (False_ind P H6)))))))))))))) i v y x H0))) H)))))).