(* Require Export Eqdep_dec.  *)
Require Import List.
Require Import Peano_dec. 
Require Import Arith.
Require Import InductiveFiniteSets.
Require Import FiniteTypes.
Require Import Containers.
Require Import Substitution.
Require Import FinSummDefs.
Require Import JMeq.

Set Implicit Arguments.


Section Ucontainers_lists.

(* the Ucontainer for lists *) 
 Definition Lst: Ucontainer :=   ucont Fin.  
 Definition pLst  (n m : nat)  := ucont (FinTimes n m) .

Section nil_and_cons.

Variable X : Set . 
(* Definition clist   := Ext Lst X. *)
     
 (* nil and cons *)
 Definition cnil := uext Lst  0 (nofin X).
 
 Definition ccons  (x: X) (xs: Ext Lst X  ) : Ext Lst X := 
           match xs with  uext u0 f0 => uext Lst (S u0) (caseFin x f0) end.

Theorem nil_not_cons : forall (x : X) (cs : Ext Lst X),  cnil <> ccons x cs.
Proof.
  intros x cs0; destruct cs0.
  unfold cnil; unfold ccons.
  intro H; destruct (ext_eq_dst H) as [H0 _ ]; 
  discriminate H0.
Qed.
 
End nil_and_cons.

Section natural_transformations_to_lists_and_back.   
 Implicit Arguments fz [n].
   
 Variable X : Set.

 (* extension to normal list *)
 Definition ext_to_list :  forall  (cl  : Ext Lst X), list X.
   intros  cl;  destruct cl. 
   induction u.  
   exact nil. 
   exact (f fz :: IHu (fun m: Fin  u => f (fs m))).
 Defined.

(* the shape is given by the length *)
Lemma ext_to_list_len  (n : nat) (G : Fin n -> X) :
    length (ext_to_list (uext Lst n G)) = n .
 Proof.
  induction n; auto. 
  intro G.
  replace (length (ext_to_list (uext Lst (S n) G))) with
       (S(length (ext_to_list (uext Lst  n (fun i => G (fs i))))));
  auto.
 Qed. 

(* positions in the list  *)
Definition typ  (l: list X) : Fin (length l) ->  X.
  intros  l j; induction  l .  
  inversion j.
  inversion  j.
  exact a.
  exact  (IHl H0).
Defined.

(* normal list to exteniosns *)
Definition list_to_ext   (l: list X) : Ext Lst X := 
   uext Lst (length l) (typ l).

(* Isomorphism form normal list to extensions *)
Lemma ext_to_LList : forall l : list X,
   ext_to_list (uext Lst (length l) (typ l))  = l .
Proof.
  induction l.
  simpl; trivial.
  pattern l at 3;
  rewrite <- IHl;
  auto.
Qed.

Lemma list_to_EExt : forall l : list X, 
     list_to_ext (ext_to_list (uext Lst (length l) (typ l)))  = uext Lst (length l) (typ l). 
Proof.
  unfold list_to_ext.
  intro l.
  apply ext_eq. 
  unfold  Containers.u. 
  rewrite <-  (ext_to_list_len (typ l)); trivial.
  unfold Containers.f; unfold Containers.u.
  apply  (dextensionality Fin (ext_to_list_len (typ l))
         (typ (ext_to_list (uext Lst (length l) (typ l)))) (typ l)).
  rewrite  (ext_to_LList l).
  intros x y H; case (JMeq_eq H);
  trivial.
Qed.

End natural_transformations_to_lists_and_back. 

Section List_functions_and_proofs.
             
Set Implicit Arguments.

Section Container_Morphisms .
   
 (* reverse *)
 Definition crev : cmr Lst Lst := uCmr Lst Lst (id (s Lst))  (fun nn: s Lst => fun Fn: p Lst nn => rv Fn).
 
Definition isSuc (n: nat) :=  match n with
                              | O => false
                              | _ => true
                              end. 
                  
Definition Fst (n: nat) (s : So (isSuc n)) : Fin n.
   intros n s1; destruct n. 
   inversion s1.
   exact (fz n).
Defined.
                 
 (* Head *)
Definition cHead  := uCmr Lst maybe_cont isSuc Fst.
                                
Definition tail_s (n:nat) : bool  + nat :=
   match n   with
   | O => inl nat false
   | S m => inr bool m
   end.           
                                                 
Definition rest (n: nat)  (q : p (cont_sum maybe_cont Lst) (tail_s n))  : Fin n.
   intros n q; destruct n.  
   inversion q.
   exact (fs q).
Defined.
               
(* Tail *)      
Definition ctail := 
    uCmr Lst  (cont_sum maybe_cont Lst )  (fun a => tail_s a)    
     (fun a : s Lst  => fun ps : p (cont_sum maybe_cont Lst) (tail_s a) => rest a ps ).

Definition not_last (n:nat) (q : p (cont_sum maybe_cont Lst) (tail_s n)) : Fin n.
  intros n q; destruct  n.  
  inversion q.  
  destruct n.    
  inversion q. 
  simpl in q; inversion q.  
  exact (emb (fz n)).
   exact (emb  q). 
Defined.

(* But_last *)
Definition cbut_lst :=
   uCmr Lst (cont_sum maybe_cont Lst) (fun a => tail_s a)
       (fun a: s Lst => fun ps : p (cont_sum maybe_cont Lst) (tail_s a) => not_last a ps).

(* append *)                       
 Definition cappend  := 
      let smap :=  (fun SP: s (cont_prod Lst  Lst) =>(fst SP + snd SP))  in 
          let pmap :=  (fun nm : s (cont_prod Lst Lst)  =>  
             fun pm: p Lst  (smap nm) => FinCase (fst nm) (snd nm) pm ) in
                 uCmr   (cont_prod Lst Lst)  Lst smap pmap .

Definition cappendl : cmr (cont_prod Lst (cont_prod Lst Lst)) Lst.
  refine (uCmr (cont_prod Lst (cont_prod Lst Lst)) Lst 
    (fun sp : nat * (nat * nat) => fst sp + fst (snd sp) + snd (snd sp))
    _ ); simpl.
  intros a H . 
  destruct a as [n p]; simpl in *. 
  destruct p as [n0 n1]; simpl in *.
  destruct (finsplit (n + n0) n1 H) as [l | r].
  destruct (finsplit n n0 l) as [i | j].
  exact (inl (Fin n0 + Fin n1) i).
  exact (inr (Fin n) (inl (Fin n1) j)).
  exact (inr (Fin n) (inr (Fin n0) r)).
Defined.

Definition cappendr : cmr (cont_prod (cont_prod Lst Lst) Lst) Lst.
  refine (uCmr (cont_prod (cont_prod Lst Lst) Lst) Lst 
    (fun sp : (nat * nat) * nat  =>  fst (fst sp) + snd (fst sp) + snd sp)
    _ ); simpl.
  intros a H.
  destruct a as [p n]; simpl in *.
  destruct p as [n0 n1]; simpl in *.
  destruct (finsplit (n0 + n1) n H) as [l | r].
  destruct (finsplit n0 n1 l) as [i | j].
  exact (inl (Fin n) (inl (Fin n1) i)).
  exact (inl (Fin n) (inr (Fin n0) j)).
  exact (inr (Fin n0 + Fin n1) r).
Defined.

  
 
Definition  cflatt_p (a: Ext Lst nat) (i : Fin (sum_n (f a))) : CPos Lst a :=
   match  (finSumm (f a) i) with
  | finPair j k => cpos Lst a j k
  end. 

(* flatten *)   
Definition cflatt := 
     let smap := (fun a : s (cComp Lst Lst)  => sum_n (f a)) in
          let pmap := (fun a : s (cComp Lst Lst) => 
             fun ps : p Lst (sum_n (f a)) => cflatt_p a ps) in
               uCmr (cComp Lst Lst) Lst smap pmap.

Definition map_rev := 
     let pmap :=  (fun a : Ext Lst nat => fun ps : CPos Lst a  => cpos Lst a (cs ps) (rv (cp ps))) in
          uCmr (cComp Lst Lst) (cComp Lst Lst) (id (Ext Lst nat))  pmap.

Fixpoint leN (n m:nat) {struct n}: bool :=
    match n with
   | O => true 
   | S n' => match m with
                  | O => false 
                  | S m' => leN n' m'
                  end
   end.

Record pairFin (n: nat) : Set := prfin {pa: Fin n  ;  pb : Fin n}.
Definition zLst := ucont (fun n => pairFin n ).     
Definition min (n m : nat) : nat := let b := leN n m in if b then n else m.        
         
 Definition zip_pos (pn: (nat * nat) ) (i: pairFin  (min (fst pn) (snd pn) )) :  Fin (fst pn) + Fin (snd pn) .
   intros pn ;  destruct pn  as [n1 n2]. 
   unfold min; destruct n1; destruct n2; simpl.
   intro i; destruct i. inversion pa0.
   intro i; destruct i. inversion pb0.
   intro i; destruct i.  inversion pa0.
  destruct (leN n1 n2) as [| tt ff]; simpl.
  intro i; exact (inl (Fin (S n2)) (pa i)). 
  intro i;exact (inr (Fin (S n1)) (pb i)).
Defined.
            
(* Zip *)
Definition czip :=  let smap :=  (fun a => min (fst a) (snd a)) in
      let pmap := (fun aa : s (cont_prod Lst Lst) =>  (fun ps: p zLst (smap aa) =>  zip_pos aa ps)) in
             uCmr (cont_prod Lst Lst) zLst smap pmap.

(* Unzip *)
Definition cunzip  := 
   uCmr zLst (cont_prod Lst Lst) (fun n : nat => pair n n) 
        (fun a : nat => fun ps : Fin a + Fin a => match ps with
                                                  | inl a => prfin a a
                                                  | inr a => prfin a a 
                                                 end).
  (* zip rev 1*)
Definition zrev := let pmap := (fun a : s zLst => fun Pz : p zLst a => prfin (rv (pa  Pz)) (rv (pb Pz))) in 
            uCmr zLst zLst (id (s zLst))  pmap.   
 
(* zip rev 2 *)
Definition czip_revr := 
    let cziprv_pmap := (fun  a : nat * nat => fun  i : p zLst (v czip a)  => zip_pos
 a (prfin (rv (pa i)) (rv (pb i)))) in 
            uCmr (cont_prod Lst Lst) zLst  (v czip) (fun a : nat * nat =>
                         fun Pcz : p zLst (v czip a) => cziprv_pmap a Pcz).

End Container_Morphisms.  
                                    
Section Container_Proofs. 

(* Reverse is idempotent *)
Theorem crev_crev_id : Eqmor (m_comp crev crev) (idm Lst).
 Proof. 
   simpl.
   unfold idm; unfold comp.
   apply morq; simpl.
   intro a; apply (refl_equal a). 
   intros a p0 p1 H;  elim  H; apply idem_rvFin.
Qed. 

(* reversing nested lists (i.e. via composing containers) is also idempotent *)
Theorem ap_crev_id : Eqmor (m_comp (ap_mor crev Lst) (ap_mor crev Lst)) (idm (cComp Lst Lst)).
Proof.
  simpl; unfold comp; unfold id.
  apply morq; simpl.
  intro a ;  
  rewrite (extensionality (fun z : Fin ( u a) => f a (rv (rv z))) (f a) 
                (fun x  :Fin (u a) => f_equal (f a) (idem_rvFin x))).
  destruct a; simpl; trivial.
  unfold id; intro a.
  cut  (a = uext Lst (u a) (fun z : Fin (u a) => f a (rv (rv z)))).
  intros H0 p0 p1 H; apply cpos_eq; simpl.
 apply (eq_subs (fun i : Fin (u a) => i = cs p1)  (sym_equal (idem_rvFin (cs p0))) ).
 Implicit Arguments cpos_Jmeq [ ].
 apply (JMeq_eq (sym_JMeq (proj1 (cpos_Jmeq Lst Lst a (uext Lst (u a) 
            (fun s : Fin (u a) => f a (rv (rv s)))) H0 p1 p0 (sym_JMeq H))))).
 apply (sym_JMeq (proj2 (cpos_Jmeq Lst Lst a (uext Lst (u a) 
     (fun s : Fin (u a) => f a (rv (rv s)))) H0 p1 p0 (sym_JMeq H)))).
 rewrite  (extensionality (fun z : Fin ( u a) => f a (rv (rv z))) (f a) 
                (fun x  :Fin (u a) => f_equal (f a) (idem_rvFin x))).
 destruct a; trivial.
Qed.

 (* zip_rev  *)
  Theorem czip_rev : Eqmor (czip_revr) (m_comp zrev czip ).
 Proof.
   apply morq; simpl; trivial. 
   unfold comp; unfold id.
   intros a p0 p1 H; elim H; trivial.
 Qed. 
                           
 (* Distributuvty of append over reverse *)
Theorem cdist_aprev : Eqmor  (m_comp cappend (m_comp (mor_prod crev crev)  (prod_swap Lst Lst))) (m_comp crev cappend).
Proof.
   simpl; unfold comp; unfold id.
   apply morq; simpl. 
   intro a; apply plus_comm .
   intros a p0 p1 jm; destruct a.
   unfold FinCase;  simpl in  * |- *. 
   rewrite (match_simpl n0 n p0).
   exact  (finsumX (refl_equal (rv p1)) (finsplit n0 n p0) (finsplit n n0 (rv p1)) jm).
 Qed.

(* append is nill *)
Theorem capp_is_nil (X : Set) (ex : Ext (cont_prod Lst Lst) X) : 
   mmap cappend ex = cnil X -> (fst (u ex)) = 0 /\ (snd (u ex)) = 0.  
 Proof.
   intros X ex; destruct ex; simpl.
   unfold comp; unfold cnil.
   intro H; injection H.
   intros H0 H1;
   case (plus_is_O (fst u) (snd u)); auto.
Qed.


(* associativity of append  *)
Lemma capp_assoc : Eqmor (m_comp cappendl (prod_swap1 Lst Lst Lst)) cappendr.
Proof.
 unfold cappendl; unfold cont_prod; simpl.
 unfold comp ; apply morq; simpl; auto.
 intros a p0 p1 H; destruct a.
 destruct p; simpl in *.
 destruct (finsplit (n0 + n1) n p0).
 destruct (finsplit n0 n1 i).
 destruct (finsplit (n0 + n1) n p1).
 destruct (finsplit n0 n1 i0).
 case (fin_inl_inject n1 i i0 
  (JMeq_eq  (fin_inl_JM n (refl_equal (n0 + n1)) (fin_inl n0 n1 i) (fin_inl n0 n1 i0)H )));
 trivial.
 case (finsplit_inl_inr i j 
      (JMeq_eq  (fin_inl_JM n (refl_equal (n0 + n1)) (fin_inl n0 n1 i) (fin_inr n0 n1 j)H )) ).
 case (finsplit_inl_inr (fin_inl n0 n1 i) j (JMeq_eq H)).
 destruct (finsplit (n0 + n1) n p1).
 destruct (finsplit n0 n1 i).
 case (finsplit_inl_inr i j   
      (sym_equal (fin_inl_inject n (fin_inr n0 n1 j) (fin_inl n0 n1 i) (JMeq_eq H))) ).
 case (fin_inr_inject n0 j j0 
     (fin_inl_inject n (fin_inr n0 n1 j) (fin_inr n0 n1 j0) (JMeq_eq H))); trivial.
 case (finsplit_inl_inr (fin_inr n0 n1 j) j0 (JMeq_eq H) ) .
 destruct (finsplit (n0 + n1) n p1).
 destruct (finsplit n0 n1 i).
 case  (finsplit_inl_inr (fin_inl n0 n1 i) j (sym_equal (JMeq_eq H)) ).
 case (finsplit_inl_inr (fin_inr n0 n1 j0) j (sym_equal (JMeq_eq H))).
 case (fin_inr_inject (n0 + n1) j j0 (JMeq_eq H)); trivial.
Qed.
 
Section  Naturality_Laws. 
(* Naturality laws  over morphisms.                              *)
(* The following functions  have the same trivial proof :        *)
(*      -- f . head = head . map f                               *) 
(*      -- map f . tail  = tail  . map f                         *) 
(*      -- map f . reverse =  reverse . map f                    *) 
(*      -- map f . flatten = flatten . map (map f)               *) 

  Variables X Y : Set.
  Variable  F : X -> Y.
 

  Theorem cmap_head (ex : Ext Lst X) : (cmap F (mmap cHead ex)) = (mor_map cHead F ex). 
  Proof.
    destruct ex; auto.
  Qed.
 
  Theorem cmap_tail (ex : Ext Lst X): cmap F (mmap ctail ex) = mor_map ctail F ex.
  Proof.
    destruct ex; auto.
  Qed. 

  Theorem cmap_rev (ex : Ext Lst X): cmap F (mmap crev ex) = mor_map crev F ex.
  Proof.
    destruct ex;  auto.
  Qed.

  Theorem cmap_flatt (ex : Ext (cComp Lst Lst) X) : cmap F (mmap cflatt ex) = mor_map cflatt F ex.
  Proof.
    destruct ex; auto.
  Qed.

  Theorem cmap_append (ex : Ext (cont_prod Lst Lst) X): (mor_map cappend F ex) =  (cmap F (mmap cappend ex)).
  Proof.
    destruct ex; auto. 
  Qed.

End Naturality_Laws.


Definition rv_elim3 (n : nat) (i : Fin n) (P : Fin n -> Fin n -> Type):
        (forall j : Fin n, j =  (rv i) ->  P (rv j) j) ->  P i (rv i) . 
   exact ( fun (n : nat) (i : Fin n) (P : Fin n -> Fin n -> Type)
     (H : forall j : Fin n, j =  (rv i) ->  P (rv j) j) =>
    eq_subs (fun x : Fin n => P x (rv i)) (idem_rvFin i) (H (rv i) (refl_equal (rv i)))).
 Qed.


(* flatten reverse *)
Theorem map_flatt_rev: Eqmor (m_comp cflatt (m_comp  map_rev (ap_mor crev Lst))) (m_comp crev cflatt).
Proof.
 simpl; unfold comp; unfold id.
 apply morq; simpl.
 apply (fun a : Ext Lst nat => sum_n_rv (f a)). 
 intros a .
 cut (sum_n (f a) = sum_n (fun a0 : Fin (u a) => f a (rv a0))). 
 intros H1 p0 p1 H; unfold cflatt_p; simpl.
 destruct a; simpl in *.
 destruct (finSumm (fun a => f (rv a)) p0); simpl. 
 apply  (rv_elim3 p1 (fun _ => fun b => cpos Lst (uext Lst u f) (rv i) (rv k) =
                                         match finSumm f b with
                                        | finPair j k0 => cpos Lst (uext Lst u f) j k0
                                        end ) ). 
 intros j H0; rewrite (rvdist p1 (sym_equal H0)) in H.
 destruct (finSumm f j); simpl.
 destruct  (finjLem f i0 k0 i k (rvdistJM H1 (finj f i0 k0) (sym_JMeq H))).
 apply cpos_eq; auto.
 apply (sym_equal (sum_n_rv (f a))).
Qed.
 
 (* reversing each inner list  is idempotent *)
Theorem map_rev_id : Eqmor (m_comp map_rev map_rev) (idm (cComp Lst Lst)).
Proof.
  simpl; unfold comp; unfold id.
  apply morq; simpl; trivial.
  intros a p0 p1 H; elim H.
  clear H; clear p1. 
  apply (eq_subs (fun x : Fin (f a (cs p0)) => cpos Lst  a (cs p0) x = p0) (sym_equal (idem_rvFin (cp p0)))).
  destruct p0; auto. 
Qed.

 
(* map_rev over nested lists *)
Theorem crev_flat : Eqmor (m_comp cflatt (m_comp (ap_mor crev Lst) map_rev))
                          (m_comp cflatt  (m_comp map_rev (ap_mor crev Lst))) .
  simpl. unfold comp; unfold id.
  apply morq; simpl; trivial. 
  intros a p0 p1 H; elim H; reflexivity. 
Qed.
   
Definition two_to1s (a : Ext Lst nat * Ext Lst nat ) : Ext (cont_prod Lst Lst) nat := 
      uext (cont_prod Lst Lst) (pair (u (fst a)) (u (snd a))) 
               (fun x : Fin (u (fst a))  + Fin (u (snd a))  => match x with
                                                               | inl z => f (fst a) z
                                                               | inr z => f (snd a) z
                                                               end).

 Definition two_to1p (a : Ext Lst nat * Ext Lst nat) (b : CPos Lst (two_to1s a)) :
                                               CPos Lst (fst a) + CPos Lst (snd a).
   unfold two_to1s; intros a b;  destruct b; simpl in *. 
   destruct  cs.
   exact (inl (CPos Lst (snd a)) (cpos Lst (fst a) f cp)).
   exact (inr (CPos Lst (fst a)) (cpos Lst (snd a) f cp)).
 Defined.

 Definition lift_2n (a : cmr (cComp (cont_prod Lst Lst) Lst) (cComp Lst Lst)) :
               cmr (cont_prod (cComp Lst Lst) (cComp Lst Lst)) (cComp Lst Lst).
    intro a; destruct a; simpl in *.
    exact (uCmr (cont_prod (cComp Lst Lst) (cComp Lst Lst)) 
          (cComp Lst Lst) (fun a: Ext Lst nat * Ext Lst nat => v (two_to1s a)) 
          (fun a H =>  (two_to1p (g (two_to1s a) H)))).
 Defined.

 
 Definition ext_app (a : Ext Lst nat * Ext Lst nat) := 
     uext Lst (u (fst a) + u (snd a)) (fun a0 : Fin (u (fst a) + u (snd a)) =>
                                           match FinCase (u (fst a)) (u (snd a)) a0 with
                                           | inl z => f (fst a) z
                                           | inr z => f (snd a) z
                                           end). 

Lemma sum_n_sim : forall a : Ext Lst nat * Ext Lst nat, 
                sum_n (f (fst a)) + sum_n (f (snd a)) =  sum_n (f  (ext_app a)).
Proof.
  intro a; destruct a; simpl in *.
  destruct e as [u0 f0]; destruct e0 as [u1 f1].
  induction u0. simpl. 
  rewrite (extensionality  f1 (fun a0 : Fin u1 => f1 a0) (fun a : Fin u1 => refl_equal (f1 a)));
  reflexivity. 
  simpl sum_n in * |- *. 
  rewrite <- plus_assoc. 
  rewrite  (IHu0 (fun i : Fin u0 => f0 (fs i))); simpl in *|-*.    
  rewrite (extensionality  
       (fun a0 : Fin (u0 + u1) => 
               match  FinCase u0 u1 a0 with
               inl z => f0 (fs z)
               | inr z => f1 z
               end)
       (fun i : Fin (u0 + u1) => 
           match FinCase (S u0) u1 (fs i) with
           | inl z => f0 z
           | inr z => f1 z
           end ) (fincaseS f0 f1)); reflexivity. 
Qed. 


Lemma fsfz_jm (n m : nat) (i : Fin m) :  n= m -> JMeq (fz n) (fs i) -> False.
Proof.
  intros n m i H; destruct H.
  intro H1; generalize (JMeq_eq H1).
  intro a; discriminate a.
Qed.

Lemma flathelp1  (e e0 : Ext Lst nat) (i i0  : Fin (u e)) (H :  i = i0)
  (A : Fin (u e) + Fin (u e0)) (H1 : A = FinCase (u e) (u e0) (fin_inl (u e) (u e0) i) )
   (a : Fin (match A  with
	       | inl z => f e z
	       | inr y => f e0 y
              end ) )  (k : Fin (f e i0)) 
 : JMeq a k ->  (forall (k1 : Fin (f e i)), JMeq a k1 -> 
  inl (CPos Lst e0) (cpos Lst e i k1) =  inl (CPos Lst e0) (cpos Lst e i0 k)) ->

   (match A as s0 return ( Fin (match s0 with
				 | inl z => f e z
				 | inr y => f e0 y
				 end) -> CPos Lst e + CPos Lst e0) 
      with
    | inl f0 =>
       fun cp0 : Fin (f e f0) => inl (CPos Lst e0) (cpos Lst e f0 cp0)
   | inr f0 =>
       fun cp0 : Fin (f e0 f0) => inr (CPos Lst e) (cpos Lst e0 f0 cp0)
   end a  =   inl (CPos Lst e0) (cpos Lst e i0 k) ).
 Proof.
   intros e e0 i  .  
   rewrite  (FinCase_inl (u e0) i).
   intros i0 h; case h.   
   intros A H;   rewrite  H.
   intros.
   apply  (H1 a (JMeq_refl a)).
 Qed. 

Lemma flathelp2  (e e0 : Ext Lst nat) (j i0  : Fin (u e0)) (H :  j = i0)
  (A : Fin (u e) + Fin (u e0)) (H1 : A = FinCase (u e) (u e0) (fin_inr (u e) (u e0) j) )
   (a : Fin (match A  with
	       | inl z => f e z
	       | inr y => f e0 y
              end ) )  (k : Fin (f e0 i0)) 
 : JMeq a k ->  (forall (k1 : Fin (f e0 j)), JMeq a k1 -> 
  inr (CPos Lst e) (cpos Lst e0 j k1) =  inr (CPos Lst e) (cpos Lst e0 i0 k)) ->

   (match A as s0 return ( Fin (match s0 with
				 | inl z => f e z
				 | inr y => f e0 y
				 end) -> CPos Lst e + CPos Lst e0) 
      with
    | inl f0 =>
       fun cp0 : Fin (f e f0) => inl (CPos Lst e0) (cpos Lst e f0 cp0)
   | inr f0 =>
       fun cp0 : Fin (f e0 f0) => inr (CPos Lst e) (cpos Lst e0 f0 cp0)
   end a  =   inr (CPos Lst e) (cpos Lst e0 i0 k) ).
 Proof.
   intros e e0 j.
   rewrite (FinCase_inr (u e) j).
   intros i0 h; case h.
   intros A H; rewrite H.
   intros.
   apply (H1 a (JMeq_refl a)).
 Qed.

(* flatten append is a container morphism  *)
Theorem cdist_apflatt : Eqmor (m_comp cflatt (lift_2n (ap_mor cappend Lst))) (m_comp cappend (mor_prod cflatt cflatt)).
 Proof.
   apply morq. 
   intro a; apply (sym_eq (sum_n_sim a)).
   simpl. unfold comp.
   intro a; destruct a; simpl; unfold comp; simpl .
   intros  p0 P1 H; unfold cflatt_p. simpl.
   destruct ( finsplit (sum_n (f e)) (sum_n (f e0)) P1).
   rewrite (FinCase_inl (sum_n (f e0)) i).
   destruct ( finSumm
              (fun a : Fin (u e + u e0) =>
               match FinCase (u e) (u e0) a with
               | inl z => f e z
               | inr z => f e0 z
               end) p0); simpl. 
  destruct (finSumm (f e) i ).
  destruct (finsplit (u e) (u e0) i0).
  destruct (finjInl_inj (f e) (f e0) i i0 k0 k H).
  apply (flathelp1 (sym_equal H0) (refl_equal ( FinCase (u e) (u e0) (fin_inl (u e) (u e0) i0))) (sym_JMeq H1) ).
  intros k1 h1; 
  case (cpos_eq (cpos Lst e i k0) (cpos Lst e i0 k1) H0 (trans_JMeq H1 h1) ); 
  trivial.
  case (finjInr_Inl_false (f e) (f e0) i j k0 k H ).
  destruct ( finSumm
              (fun a : Fin (u e + u e0) =>
               match FinCase (u e) (u e0) a with
               | inl z => f e z
               | inr z => f e0 z
               end) p0); simpl. 
  rewrite (FinCase_inr (sum_n (f e)) j).
  destruct (finSumm (f e0) j ).
  destruct (finsplit (u e) (u e0) i).
  case  (finjInl_Inr_false (f e) (f e0) i i0 k0 k H).
  destruct (finjInr_inj (f e) (f e0) j i0 k0 k H ).
  apply  (flathelp2 H0 (refl_equal ( FinCase (u e) (u e0) (fin_inr (u e) (u e0) j))) (sym_JMeq H1)).
  intros k1 H2;
  case (cpos_eq (cpos Lst e0 j k1) (cpos Lst e0 i0 k0) H0 (sym_JMeq (trans_JMeq H1 H2)) );
  trivial.
 Qed.
 
End Container_Proofs.