- [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);]]
+ [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);]]