C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C
c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).
C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow
False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C
c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).