with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
(CSort n) H4) in (False_ind (eq C (CHead c2 k u2) (CHead c1 k u1))
H5))))))))))) y x H0))) H))).
with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I
(CSort n) H4) in (False_ind (eq C (CHead c2 k u2) (CHead c1 k u1))
H5))))))))))) y x H0))) H))).