- apply (sandwich {[l,u]} ≪?, h≫ Xi Yi Ai); [4: assumption;]
- [1: intro j; cases (Hxy j); cases H3; cases H4; split;
- [apply (H5 0);|apply (H7 0)]
- |2: cases (H l u Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
- cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
- exists [apply w] apply H7;
- |3: cases (H l u Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
- cases H4; split; [apply H5] intros (y Hy);cases (H6 (\fst y));[2:apply Hy];
- exists [apply w] apply H7;]]
+ apply (sandwich {[s]} ≪x, h≫ Xi Yi Ai); [4: assumption;]
+ [1: intro j; cases (Hxy j); cases H3; cases H4; split; clear H3 H4; simplify in H5 H7;
+ [apply (l2sl ? s (Xi j) (Ai j) (H5 0));|apply (l2sl ? s (Ai j) (Yi j) (H7 0))]
+ |2: cases (H s Xi ≪?,h≫) (Ux Uy); apply Ux; cases Hx; split; [intro i; apply (l2sl ? s (Xi i) (Xi (S i)) (H3 i));]
+ cases H4; split; [intro i; apply (l2sl ? s (Xi i) ≪x,h≫ (H5 i))]
+ intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s ? y Hy)]
+ exists [apply w] apply (x2sx ? s (Xi w) y H7);
+ |3: cases (H s Yi ≪?,h≫) (Ux Uy); apply Uy; cases Hy; split; [intro i; apply (l2sl ? s (Yi (S i)) (Yi i) (H3 i));]
+ cases H4; split; [intro i; apply (l2sl ? s ≪x,h≫ (Yi i) (H5 i))]
+ intros (y Hy);cases (H6 (\fst y));[2:apply (sx2x ? s y ≪x,h≫ Hy)]
+ exists [apply w] apply (x2sx ? s y (Yi w) H7);]]