+cases Hl (e1 e2); cases e1 (an Han); cases e2 (bn Hbn); clear Hl e1 e2;
+cases Han (SSan SIxan); cases Hbn (SSbn SIxbn); clear Han Hbn;
+cases SIxan (LBxan Hxg); cases SIxbn (UPxbn Hxl); clear SIxbn SIxan;
+change in UPxbn:(%) with (x is_lower_bound bn in ml);
+unfold upper_bound in UPxbn LBxan; change
+intros (e He);
+(* 2.6 OC *)