\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Arith.Nat
\import Data.Array
\import Data.Fin (fsuc/=, nat_fin_=)
\import Data.Or
\import Equiv
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin

\class GradedCRing \extends CRing {
  | isHomogen : E -> Nat -> \Prop
  | homogen-zro {n : Nat} : isHomogen  n
  | homogen-negative_ide : isHomogen -1 
  | homogen-+ {n : Nat} {a b : E} : isHomogen a n -> isHomogen b n -> isHomogen (a + b) n
  | homogen-* {n m : Nat} {a b : E} : isHomogen a n -> isHomogen b m -> isHomogen (a * b) (n Nat.+ m)
  | homogen-decomp (x : E) : ∃ (l : Array E) (\Pi (n : Fin l.len) -> isHomogen (l n) n) (BigSum l = x)
  | homogen-unique (l : Array E) : (\Pi (n : Fin l.len) -> isHomogen (l n) n) -> BigSum l =  -> ∀ (x : l) (x = )

  \func isHomogenArray (l : Array E) => \Pi (n : Fin l.len) -> isHomogen (l n) n

  \lemma homogen-ide : isHomogen  
    => transport (isHomogen __ ) equation (homogen-* homogen-negative_ide homogen-negative_ide)

  \lemma homogen-negative {n : Nat} {x : E} (xh : isHomogen x n) : isHomogen (negative x) n
    => transport (isHomogen __ n) equation (homogen-* homogen-negative_ide xh)

  \lemma homogen-pow {a : E} {n m : Nat} (ah : isHomogen a n) : isHomogen (pow a m) (n Nat.* m) \elim m
    |  => homogen-ide
    | suc m => homogen-* (homogen-pow ah) ah

  \lemma homogen-BigSum {l : Array E} {n : Nat} (p : ∀ (a : l) (isHomogen a n)) : isHomogen (BigSum l) n \elim l
    | nil => homogen-zro
    | a :: l => homogen-+ (p ) (homogen-BigSum (\lam j => p (suc j)))

  \lemma homogen-FinSum {J : FinSet} {a : J -> E} {n : Nat} (p : \Pi (j : J) -> isHomogen (a j) n) : isHomogen (FinSum a) n
    => \case FinSum_char a \with {
      | inP (e,q) => transportInv (isHomogen __ n) q $ homogen-BigSum \lam j => p (e j)
    }

  \lemma homogen-similar {l l' : Array E} (lh : isHomogenArray l) (l'h : isHomogenArray l') (p : BigSum l = BigSum l') : Similar l l'
    => diff=0->similar $ homogen-unique (diff l l') (diff-homogen l l'  lh l'h) (diff-sum l l' *> toZero p)
    \where {
      \func diff (l l' : Array E) : Array E \elim l, l'
        | nil, l' => map negative l'
        | a :: l, nil => a :: l
        | a :: l, a' :: l' => a - a' :: diff l l'

      \lemma diff=0->similar {l l' : Array E} (p : \Pi (j : Fin (DArray.len {diff l l'})) -> diff l l' j = ) : Similar l l' \elim l, l'
        | nil, nil => nil-nil-similar
        | nil, a :: l' => nil-::-similar (inv negative-isInv *> pmap negative (p ) *> negative_zro) $ diff=0->similar \lam j => p (suc j)
        | a :: nil, nil => ::-nil-similar (p ) nil-nil-similar
        | a :: a' :: l, nil => ::-nil-similar (p ) $ diff=0->similar \lam j => p (suc j)
        | a :: l, a' :: l' => ::-::-similar (fromZero $ p ) $ diff=0->similar \lam j => p (suc j)

      \lemma diff-sum (l l' : Array E) : BigSum (diff l l') = BigSum l - BigSum l' \elim l, l'
        | nil, l' => inv $ zro-left *> BigSum_negative
        | a :: l, nil => simplify
        | a :: l, a' :: l' => equation {usingOnly (diff-sum l l')}

      \lemma diff-homogen (l l' : Array E) (k : Nat)
                          (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (k Nat.+ j))
                          (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (k Nat.+ j))
                          (j : Fin (DArray.len {diff l l'})) : isHomogen (diff l l' j) (k Nat.+ j) \elim l, l', j
        | nil, a :: l',  => homogen-negative (l'h )
        | nil, a :: l', suc j => homogen-negative (l'h (suc j))
        | a :: l, nil,  => lh 
        | a :: a' :: l, nil, suc j => diff-homogen (a' :: l) nil (suc k) (\lam j => lh (suc j)) (\case __) j
        | a :: l, a' :: l',  => homogen-+ (lh ) (homogen-negative (l'h ))
        | a :: l, a' :: l', suc j => diff-homogen l l' (suc k) (\lam j => lh (suc j)) (\lam j => l'h (suc j)) j
    }

  \func degree-unique {a : E} {n m : Nat} (ahn : isHomogen a n) (ahm : isHomogen a m) : Or (a = ) (n = m)
    => \case decideEq n m \with {
      | yes e => inr e
      | no q => inl $ rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc m} n) in
          \let l => array2 n m a (negative a)
          \in homogen-unique l (\lam j => mcases \with {
            | yes p, d => rewriteI p ahn
            | no n1, yes p => rewriteI p (homogen-negative ahm)
            | no n1, no n2 => homogen-zro
          }) (sum-lem2 {_} {l} (fin-inc {suc n} {suc m} n) (fin-inc-right {suc n} {suc m} m)
                (\lam p => q $ inv (fin-inc.char_nat {suc m} n) *> p *> fin-inc-right.char_nat {suc n} m)
                (\lam k p1 p2 => rewrite (decideEq/=_reduce \lam p => p1 $ fin_nat-inj $ inv $ fin-inc.char_nat {suc m} n *> p, decideEq/=_reduce \lam p => p2 $ fin_nat-inj $ inv $ fin-inc-right.char_nat {suc n} m *> p) idp)
              *> rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc m} n, decideEq=_reduce $ inv $ fin-inc-right.char_nat {suc n} m, decideEq/=_reduce \lam p => q $ p *> fin-inc-right.char_nat {suc n} m) negative-right) (fin-inc {suc n} {suc m} n)
    } \where {
      \func array2 (n m : Nat) (a b : E) => \new Array E (suc n Nat.+ suc m) \lam j => \case decideEq n j, decideEq m j \with {
        | yes _, _ => a
        | no _, yes _ => b
        | no _, no _ => 
      }

      \lemma sum-lem1 {l : Array E} (i : Fin l.len) (c : \Pi (k : Fin l.len) -> k /= i -> l k = ) : BigSum l = l i \elim l, i
        | a :: l,  => pmap (a +) (BigSum_zro \lam j => c (suc j) (\case __)) *> zro-right
        | a :: l, suc i => pmap (`+ _) (c  \case __) *> zro-left *> sum-lem1 i (\lam k d => c (suc k) (fsuc/= d))

      \lemma sum-lem2 {l : Array E} (i j : Fin l.len) (i/=j : i /= j) (c : \Pi (k : Fin l.len) -> k /= i -> k /= j -> l k = ) : BigSum l = l i + l j \elim l, i, j
        | nil, i, _ => \case i
        | a :: l, ,  => \case i/=j idp
        | a :: l, , suc j => pmap (a +) (sum-lem1 j \lam k d => c (suc k) (\case __) (fsuc/= d))
        | a :: l, suc i,  => pmap (a +) (sum-lem1 i \lam k d => c (suc k) (fsuc/= d) (\case __)) *> +-comm
        | a :: l, suc i, suc j => pmap (`+ _) (c  (\case __) (\case __)) *> zro-left *> sum-lem2 i j (\lam p => i/=j \lam i => suc (p i)) (\lam k d1 d2 => c (suc k) (fsuc/= d1) (fsuc/= d2))
  }

  \func degree-unique2 {a b c : E} {n m k : Nat} (p : a = b + c) (ah : isHomogen a n) (bh : isHomogen b m) (ch : isHomogen c k) : Or (Or (b = ) (c = )) (m = k)
    => \case decideEq m k \with {
      | yes m=k => inr m=k
      | no m/=k => \let | l => degree-unique.array2 m k b c
                        | s => homogen-similar {_} {l} {replicate n zro ++ a :: nil} (\lam j => mcases \with {
                            | yes e, d => rewriteI e bh
                            | no _, yes e => rewriteI e ch
                            | no n1, no n2 => homogen-zro
                          }) (homogen-++ (\lam j => homogen-zro) $ later \lam () => ah) $
                          degree-unique.sum-lem2 {_} {l} (fin-inc {suc m} {suc k} m) (fin-inc-right {suc m} {suc k} k)
                              (\lam p => m/=k $ inv (fin-inc.char_nat {suc k} m) *> p *> fin-inc-right.char_nat {suc m} k)
                              (\lam l p1 p2 => rewrite (decideEq/=_reduce \lam p => p1 $ fin_nat-inj $ inv $ fin-inc.char_nat {suc k} m *> p, decideEq/=_reduce \lam p => p2 $ fin_nat-inj $ inv $ fin-inc-right.char_nat {suc m} k *> p) idp)
                          *> rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc k} m, decideEq=_reduce $ inv $ fin-inc-right.char_nat {suc m} k, decideEq/=_reduce \lam p => m/=k $ p *> fin-inc-right.char_nat {suc m} k) (inv p) *> inv (BigSum_++ *> pmap (`+ _) BigSum_replicate0 *> simplify)
                   \in \case decideEq n m \with {
                     | yes n=m => cases (decideEq m (fin-inc-right {suc m} k), decideEq k (fin-inc-right {suc m} k), similar-unique l a n s (fin-inc-right {suc m} {suc k} k) \lam p => m/=k $ inv n=m *> p *> fin-inc-right.char_nat {suc m} k) \with {
                         | yes e, _, t => inl (inl t)
                         | no n1, yes e, t => inl (inr t)
                         | no _, no c, t => absurd $ c $ inv $ fin-inc-right.char_nat {suc m} k
                       }
                     | no n/=m => inl $ inl $ rewrite (decideEq=_reduce $ inv $ fin-inc.char_nat {suc k} m) in similar-unique l a n s (fin-inc {suc m} {suc k} m) \lam p => n/=m $ p *> fin-inc.char_nat {suc k} m
                   }
    }
    \where {
      \lemma similar-unique (l : Array E) (a : E) (n : Nat) (s : Similar l (replicate n zro ++ a :: nil)) (j : Fin l.len) (n/=j : n /= j) : l j =  \elim l, n, s, j
        | a' :: l, , ::-::-similar p s,  => absurd (n/=j idp)
        | a' :: l, , ::-::-similar p s, suc j => similar-nil s j
        | a' :: l, suc n, ::-::-similar p s,  => p
        | a' :: l, suc n, ::-::-similar p s, suc j => similar-unique l a n s j \lam q => n/=j (pmap suc q)
    }

  \func homogenSum-unique {l : Array E} (lh : isHomogenArray l) {n : Nat} (h : isHomogen (BigSum l) n)
    : Or (\Sigma (j : Fin l.len) (BigSum l = l j) (j = {Nat} n)) (BigSum l = )
    => \case similar-eq (homogen-similar {_} {replicate n zro ++ BigSum l :: nil} (homogen-++ (\lam j => homogen-zro) $ later \lam () => h) lh $
              BigSum_++ *> pmap2 (+) BigSum_replicate0 zro-right *> zro-left) (++.index-right ) \with {
         | inl r => inl (r., inv ++.++_index-right *> r., r. *> ++.index-right-nat)
         | inr r => inr (inv ++.++_index-right *> r)
       }

  \lemma homogen-++ {l l' : Array E} (lh : isHomogenArray l) (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (l.len Nat.+ j)) : isHomogenArray (l ++ l')
    => aux  lh l'h
    \where
      \lemma aux {l l' : Array E} (n : Nat)
                 (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j))
                 (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (n Nat.+ l.len Nat.+ j))
                 (j : Fin (DArray.len {l ++ l'}))
        : isHomogen (++ l l' j) (n Nat.+ j) \elim l, j
        | nil, j => l'h j
        | a :: l,  => lh 
        | a :: l, suc j => aux (suc n) (\lam j => lh (suc j)) l'h j

  \lemma homogen-factor {a b c : E} (b=ac : b = a * c) {n m : Nat} (bh : isHomogen b n) (ah : isHomogen a m)
    : ∃ (c' : E) (k : Nat) (isHomogen c' k) (b = a * c')
    => TruncP.map (homogen-decomp c) \lam (l,lh,+l=c) => aux n m  lh $ homogen-similar
         (homogen-++ (\lam j => homogen-zro) $ later \lam () => bh)
         (homogen-++ (\lam j => homogen-zro) $ later \lam j => homogen-* ah (lh j))
         (BigSum_++ *> pmap (`+ _) BigSum_replicate0 *> later (simplify $ b=ac *> pmap (a *) (inv +l=c) *> BigSum-ldistr) *> inv (BigSum_++ *> pmap (`+ _) BigSum_replicate))
    \where {
      \func aux {a b : E} (s t n : Nat) {l : Array E} (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j)) (p : Similar (replicate s zro ++ b :: nil) (replicate t zro ++ map (a *) l))
        : \Sigma (c : E) (k : Nat) (isHomogen c k) (b = a * c) \elim s, t, l, p
        | , , nil, ::-nil-similar idp _ => (, , homogen-zro, inv zro_*-right)
        | , , c :: l, ::-::-similar p _ => (c, n, lh , p)
        | , suc t, l, ::-::-similar idp _ => (, , homogen-zro, inv zro_*-right)
        | suc s, , nil, ::-nil-similar _ q => aux s  n lh q
        | suc s, , c :: l, ::-::-similar _ q => aux s  (suc n) (\lam j => lh (suc j)) q
        | suc s, suc t, l, ::-::-similar _ q => aux s t n lh q
    }

  \lemma homogen-factor2 {a1 a2 b c d : E} (b=ac : b = a1 * c + a2 * d) {n m1 m2 : Nat} (bh : isHomogen b n) (a1h : isHomogen a1 m1) (a2h : isHomogen a2 m2)
    : ∃ (c' d' : E) (k1 k2 : Nat) (isHomogen c' k1) (isHomogen d' k2) (b = a1 * c' + a2 * d')
    => \case homogen-decomp c, homogen-decomp d \with {
      | inP (l1,l1h,+l1=c1), inP (l2,l2h,+l2=c2) => inP $ aux n m1 m2   l1h l2h $ homogen-similar
          (homogen-++ (\lam j => homogen-zro) $ later \lam () => bh)
          (homogen-sum  (homogen-++ (\lam j => homogen-zro) (\lam j => later $ homogen-* a1h (l1h j))) (homogen-++ (\lam j => homogen-zro) (\lam j => later $ homogen-* a2h (l2h j))))
          $ BigSum_++ *> pmap (`+ _) BigSum_replicate0 *> simplify b=ac *>
            inv (BigSum_sum *> pmap2 (+) (BigSum_++ *> pmap (`+ _) BigSum_replicate0 *> zro-left) (BigSum_++ *> pmap (`+ _) BigSum_replicate0 *> zro-left) *> pmap2 (+) (inv BigSum-ldistr *> pmap (a1 *) +l1=c1) (inv BigSum-ldistr *> pmap (a2 *) +l2=c2))
    }
    \where {
      \func sum (l l' : Array E) : Array E \elim l, l'
        | nil, l' => l'
        | a :: l, nil => a :: l
        | a :: l, a' :: l' => a + a' :: sum l l'

      \lemma sum_nil {l : Array E} : sum l nil = l \elim l
        | nil => idp
        | a :: l => idp

      \lemma BigSum_sum {l l' : Array E} : BigSum (sum l l') = BigSum l + BigSum l' \elim l, l'
        | nil, nil => inv zro-left
        | nil, a :: l => inv zro-left
        | a :: l, nil => inv zro-right
        | a :: l, a' :: l' => pmap (_ +) BigSum_sum *> equation

      \lemma homogen-sum {l l' : Array E} (n : Nat)
                         (lh : \Pi (j : Fin l.len) -> isHomogen (l j) (n Nat.+ j))
                         (l'h : \Pi (j : Fin l'.len) -> isHomogen (l' j) (n Nat.+ j))
                         (j : Fin (DArray.len {sum l l'}))
        : isHomogen (sum l l' j) (n Nat.+ j) \elim l, l', j
        | nil, a :: l,  => l'h 
        | nil, a :: l, suc j => l'h (suc j)
        | a :: l, nil,  => lh 
        | a :: l, nil, suc j => lh (suc j)
        | a :: l, a' :: l',  => homogen-+ (lh ) (l'h )
        | a :: l, a' :: l', suc j => homogen-sum (suc n) (\lam j => lh (suc j)) (\lam j => l'h (suc j)) j

      \func aux {a1 a2 b : E} (s t1 t2 n1 n2 : Nat) {l1 l2 : Array E}
                (l1h : \Pi (j : Fin l1.len) -> isHomogen (l1 j) (n1 Nat.+ j))
                (l2h : \Pi (j : Fin l2.len) -> isHomogen (l2 j) (n2 Nat.+ j))
                (p : Similar (replicate s zro ++ b :: nil) (sum (replicate t1 zro ++ map (a1 *) l1) (replicate t2 zro ++ map (a2 *) l2)))
        : \Sigma (c1 c2 : E) (k1 k2 : Nat) (isHomogen c1 k1) (isHomogen c2 k2) (b = a1 * c1 + a2 * c2) \elim s, t1, t2, l1, l2, p
        | , , , nil, nil, ::-nil-similar p _ => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , , , nil, c2 :: l2, ::-::-similar p q => (, c2, , n2, homogen-zro, l2h , p *> simplify)
        | , , , c1 :: l1, nil, ::-::-similar p q => (c1, , n1, , l1h , homogen-zro, p *> simplify)
        | , , , c1 :: l1, c2 :: l2, ::-::-similar p _ => (c1, c2, n1, n2, l1h , l2h , p)
        | , , suc t2, nil, _, ::-::-similar p _ => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , , suc t2, c1 :: l1, _, ::-::-similar p q => (c1, , n1, , l1h , homogen-zro, p *> simplify)
        | , suc t1, , _, nil, ::-::-similar p q => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | , suc t1, , _, c2 :: l2, ::-::-similar p q => (, c2, , n2, homogen-zro, l2h , p *> simplify)
        | , suc t1, suc t2, l1, l2, ::-::-similar p q => (, , , , homogen-zro, homogen-zro, p *> simplify)
        | suc s, , , nil, nil, ::-nil-similar _ q => aux s   n1 n2 l1h l2h q
        | suc s, , , nil, c2 :: l2, ::-::-similar _ q => aux s   n1 (suc n2) l1h (\lam j => l2h (suc j)) q
        | suc s, , , c1 :: l1, nil, ::-::-similar _ q => aux s   (suc n1) n2 (\lam j => l1h (suc j)) l2h (rewrite sum_nil q)
        | suc s, , , c1 :: l1, c2 :: l2, ::-::-similar _ q => aux s   (suc n1) (suc n2) (\lam j => l1h (suc j)) (\lam j => l2h (suc j)) q
        | suc s, , suc t2, nil, l2, ::-::-similar _ q => aux s  t2 n1 n2 l1h l2h q
        | suc s, , suc t2, c1 :: l1, l2, ::-::-similar _ q => aux s  t2 (suc n1) n2 (\lam j => l1h (suc j)) l2h q
        | suc s, suc t1, , l1, nil, ::-::-similar _ q => aux s t1  n1 n2 l1h l2h (rewrite sum_nil q)
        | suc s, suc t1, , l1, c2 :: l2, ::-::-similar _ q => aux s t1  n1 (suc n2) l1h (\lam j => l2h (suc j)) q
        | suc s, suc t1, suc t2, l1, l2, ::-::-similar _ q => aux s t1 t2 n1 n2 l1h l2h q
    }

  \lemma FinSum-homogen {J : FinSet} {a : J -> E} (p : \Pi (j : J) -> \Sigma (n : Nat) (isHomogen (a j) n)) : FinSum a = BigSum array
    => FinSum_Equiv (later \new QEquiv {
      | f s => s..
      | ret j => ((p j)., (j, inv $ mod_< $ FinJoin-cond _ <∘r id<suc))
      | ret_f => unfold $ unfold $ unfold \lam s => exts (nat_fin_= $ mod_< (FinJoin-cond s.. <∘r id<suc) *> s.., idp)
      | f_sec j => idp
    }) *> inv (FinSum-double-dep (\lam i => SigmaFin J \lam j => DecFin (decideEq (p j). i)) {\lam s => a s..}) *> FinSum=BigSum {_} {suc $ FinJoin (\lam j => (p j).)}
    \where {
      \func array => \new Array E (suc $ FinJoin (\lam j => (p j).)) \lam i => FinSum {_} {SigmaFin J \lam j => DecFin (decideEq (p j). i)} (\lam k => a k.)

      \lemma array-homogen : isHomogenArray array
        => \lam n => homogen-FinSum $ later \lam j => transport (isHomogen _) j. (p j.).
    }

  \lemma sum-decomp (l : Array (\Sigma E E)) (c : \Pi (i : Fin l.len) -> ∃ (n : Nat) (isHomogen (l i). n))
    : ∃ (N : Nat) (f : \Pi (n : Fin N) -> \Sigma (J : FinSet) (g : J -> E) (\Pi (j : J) -> \Sigma (n : Nat) (isHomogen (g j) n)) (h : J -> Fin l.len) (\Pi (j : J) -> isHomogen (g j * (l (h j)).) n))
        (BigSum (map (\lam s => s. * s.) l) = BigSum (\lam n => FinSum (\lam j => (f n). j * (l ((f n). j)).)))
    => \let | (inP c') => FinSet.finiteAC c
            | (inP d) => FinSet.finiteAC (\lam i => homogen-decomp (l i).)
            | p k : _ => later $ (k. Nat.+ (c' k.)., homogen-* ((d k.). k.) (c' k.).)
            | q => path (\lam i => BigSum (\lam i' => inv (FinSum=BigSum *> (d i').) i * (l i').)) *> inv FinSum=BigSum *>
                   pmap FinSum (ext \lam j => FinSum-rdistr) *> FinSum-double-dep (\lam i => FinFin (DArray.len {(d i).})) *> FinSum-homogen p
       \in inP (suc _, \lam n => (SigmaFin (SigmaFin (FinFin l.len) (\lam i => FinFin (DArray.len {(d i).}))) (\lam k => DecFin (decideEq (p k). n)), \lam k => (d k..). k.., \lam k => (k.., (d k..). k..), __.., \lam k => transport (isHomogen _) k. (p k.).), q)
} \where {
  \open Bounded.JoinSemilattice

  \data Similar {A : AddPointed} (l l' : Array A) \elim l, l'
    | nil, nil => nil-nil-similar
    | nil, a :: l' => nil-::-similar (a = ) (Similar nil l')
    | a :: l, nil => ::-nil-similar (a = ) (Similar l nil)
    | a :: l, a' :: l' => ::-::-similar (a = a') (Similar l l')

  \lemma similar-nil {A : AddPointed} {l : Array A} (s : Similar l nil) (j : Fin l.len) : l j =  \elim l, s, j
    | a :: l, ::-nil-similar p s,  => p
    | a :: l, ::-nil-similar p s, suc j => similar-nil s j

  \func similar-eq {A : AddPointed} {l l' : Array A} (s : Similar l l') (j : Fin l.len)
    : Or (\Sigma (i : Fin l'.len) (l j = l' i) (i = {Nat} j)) (l j = ) \elim l, l', s, j
    | a :: l, nil, ::-nil-similar p s,  => inr p
    | a :: l, nil, ::-nil-similar p s, suc j => \case similar-eq s j \with {
      | inl r => \case r.
      | inr r => inr r
    }
    | a :: l, a' :: l', ::-::-similar p s,  => inl (, p, idp)
    | a :: l, a' :: l', ::-::-similar p s, suc j => \case similar-eq s j \with {
      | inl r => inl (suc r., r., pmap suc r.)
      | inr r => inr r
    }
}