x1)).(\lambda (H9: (csubc g e1 x1)).(ex_intro2 C (\lambda (e2: C).(getl i c2
e2)) (\lambda (e2: C).(csubc g e1 e2)) x1 (getl_intro i c2 x1 x0 H5 H8)
H9)))) H7)))))) H4)))))) H1)))))))).
x1)).(\lambda (H9: (csubc g e1 x1)).(ex_intro2 C (\lambda (e2: C).(getl i c2
e2)) (\lambda (e2: C).(csubc g e1 e2)) x1 (getl_intro i c2 x1 x0 H5 H8)
H9)))) H7)))))) H4)))))) H1)))))))).