_) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H5) in (False_ind (ex2 C
(\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v)))
(\lambda (e2: C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H))))).
_) \Rightarrow False])])) I (CHead e1 (Bind Abbr) v) H5) in (False_ind (ex2 C
(\lambda (e2: C).(eq C (CHead c3 (Bind Abbr) u) (CHead e2 (Bind Abbr) v)))
(\lambda (e2: C).(csubt g e1 e2))) H6))))))))))) y c2 H0))) H))))).