--#include "alfa/SPS.alfa"

open Identity
 use  Identical,  (==),  refl,  subst,  substSym,  sym,  trans,  cong,
      cong2,  cong1

open Module_Prelude  use  zip,  List,  Tuple2,  fst,  snd

open Module_SPS
 use  S,  feed,  runS,  mapS,  mapAccumS,  (>*<),  (-<-),
      Separation1,  Separation2,  rights,  lefts,  split,  (>+<),
      Separation3

proofSeparation1 (t148::Star)
                 (t145::Star)
                 (t149::Star)
                 (t147::Star)
                 (sps1::S t148 t145)
                 (sps2::S t149 t147)
                 (is1::List t148)
                 (is2::List t149)
  :: Identical (Module_Prelude.List (Module_Prelude.Tuple2 t145 t147))
       (runS (Module_Prelude.Tuple2 t148 t149)
          (Module_Prelude.Tuple2 t145 t147)
          ((>*<) t148 t145 t149 t147 sps1 sps2)
          (zip t148 t149 is1 is2))
       (zip t145 t147 (runS t148 t145 sps1 is1) (runS t149 t147 sps2 is2))
  = case is1 of {
      (Nil) -> Ref@_;
      (Cons x xs) ->
        case is2 of {
          (Nil) -> Ref@_;
          (Cons x' xs') ->
            cong (Module_Prelude.List (Module_Prelude.Tuple2 t145 t147))
              (Module_Prelude.List (Module_Prelude.Tuple2 t145 t147))
              (runS (Module_Prelude.Tuple2 t148 t149)
                 (Module_Prelude.Tuple2 t145 t147)
                 (Module_Prelude.snd (Module_Prelude.Tuple2 t145 t147)
                    (S (Module_Prelude.Tuple2 t148 t149)
                       (Module_Prelude.Tuple2 t145 t147))
                    (feed (Module_Prelude.Tuple2 t148 t149)
                       (Module_Prelude.Tuple2 t145 t147)
                       ((>*<) t148 t145 t149 t147 sps1 sps2)
                       (Tuple2@_ x x')))
                 (zip t148 t149 xs xs'))
              (zip t145 t147
                 (runS t148 t145
                    (Module_Prelude.snd t145 (S t148 t145)
                       (feed t148 t145 sps1 x))
                    xs)
                 (runS t149 t147
                    (Module_Prelude.snd t147 (S t149 t147)
                       (feed t149 t147 sps2 x'))
                    xs'))
              (\(h::List (Module_Prelude.Tuple2 t145 t147)) ->
               Cons@_
                 (fst (Module_Prelude.Tuple2 t145 t147)
                    (S (Module_Prelude.Tuple2 t148 t149)
                       (Module_Prelude.Tuple2 t145 t147))
                    (feed (Module_Prelude.Tuple2 t148 t149)
                       (Module_Prelude.Tuple2 t145 t147)
                       ((>*<) t148 t145 t149 t147 sps1 sps2)
                       (Tuple2@_ x x')))
                 h)
              (proofSeparation1 t148 t145 t149 t147
                 (snd t145 (S t148 t145) (feed t148 t145 sps1 x))
                 (snd t147 (S t149 t147) (feed t149 t147 sps2 x'))
                 xs
                 xs');};}
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "proofSeparation1" hide 4
 #-}