\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 0 n | homogen-negative_ide : isHomogen -1 0 | 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 = 0 -> ∀ (x : l) (x = 0) \func isHomogenArray (l : Array E) => \Pi (n : Fin l.len) -> isHomogen (l n) n \lemma homogen-ide : isHomogen 1 0 => transport (isHomogen __ 0) 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 | 0 => 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 0) (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' 0 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 = 0) : Similar l l' \elim l, l' | nil, nil => nil-nil-similar | nil, a :: l' => nil-::-similar (inv negative-isInv *> pmap negative (p 0) *> negative_zro)$ diff=0->similar \lam j => p (suc j)
| a :: nil, nil => ::-nil-similar (p 0) nil-nil-similar
| a :: a' :: l, nil => ::-nil-similar (p 0) $diff=0->similar \lam j => p (suc j) | a :: l, a' :: l' => ::-::-similar (fromZero$ p 0) $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', 0 => homogen-negative (l'h 0)
| nil, a :: l', suc j => homogen-negative (l'h (suc j))
| a :: l, nil, 0 => lh 0
| a :: a' :: l, nil, suc j => diff-homogen (a' :: l) nil (suc k) (\lam j => lh (suc j)) (\case __) j
| a :: l, a' :: l', 0 => homogen-+ (lh 0) (homogen-negative (l'h 0))
| 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 = 0) (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 _ => 0 } \lemma sum-lem1 {l : Array E} (i : Fin l.len) (c : \Pi (k : Fin l.len) -> k /= i -> l k = 0) : BigSum l = l i \elim l, i | a :: l, 0 => pmap (a +) (BigSum_zro \lam j => c (suc j) (\case __)) *> zro-right | a :: l, suc i => pmap (+ _) (c 0 \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 = 0) : BigSum l = l i + l j \elim l, i, j | nil, i, _ => \case i | a :: l, 0, 0 => \case i/=j idp | a :: l, 0, suc j => pmap (a +) (sum-lem1 j \lam k d => c (suc k) (\case __) (fsuc/= d)) | a :: l, suc i, 0 => pmap (a +) (sum-lem1 i \lam k d => c (suc k) (fsuc/= d) (\case __)) *> +-comm | a :: l, suc i, suc j => pmap (+ _) (c 0 (\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 = 0) (c = 0)) (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 (0) => 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 = 0 \elim l, n, s, j
| a' :: l, 0, ::-::-similar p s, 0 => absurd (n/=j idp)
| a' :: l, 0, ::-::-similar p s, suc j => similar-nil s j
| a' :: l, suc n, ::-::-similar p s, 0 => 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 = 0)
=> \case similar-eq (homogen-similar {_} {replicate n zro ++ BigSum l :: nil} (homogen-++ (\lam j => homogen-zro) $later \lam (0) => h) lh$
BigSum_++ *> pmap2 (+) BigSum_replicate0 zro-right *> zro-left) (++.index-right 0) \with {
| inl r => inl (r.1, inv ++.++_index-right *> r.2, r.3 *> ++.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 0 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, 0 => lh 0
| 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 0 lh $homogen-similar (homogen-++ (\lam j => homogen-zro)$ later \lam (0) => 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
| 0, 0, nil, ::-nil-similar idp _ => (0, 0, homogen-zro, inv zro_*-right)
| 0, 0, c :: l, ::-::-similar p _ => (c, n, lh 0, p)
| 0, suc t, l, ::-::-similar idp _ => (0, 0, homogen-zro, inv zro_*-right)
| suc s, 0, nil, ::-nil-similar _ q => aux s 0 n lh q
| suc s, 0, c :: l, ::-::-similar _ q => aux s 0 (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 0 0 l1h l2h$ homogen-similar
(homogen-++ (\lam j => homogen-zro) $later \lam (0) => bh) (homogen-sum 0 (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, 0 => l'h 0
| nil, a :: l, suc j => l'h (suc j)
| a :: l, nil, 0 => lh 0
| a :: l, nil, suc j => lh (suc j)
| a :: l, a' :: l', 0 => homogen-+ (lh 0) (l'h 0)
| 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
| 0, 0, 0, nil, nil, ::-nil-similar p _ => (0, 0, 0, 0, homogen-zro, homogen-zro, p *> simplify)
| 0, 0, 0, nil, c2 :: l2, ::-::-similar p q => (0, c2, 0, n2, homogen-zro, l2h 0, p *> simplify)
| 0, 0, 0, c1 :: l1, nil, ::-::-similar p q => (c1, 0, n1, 0, l1h 0, homogen-zro, p *> simplify)
| 0, 0, 0, c1 :: l1, c2 :: l2, ::-::-similar p _ => (c1, c2, n1, n2, l1h 0, l2h 0, p)
| 0, 0, suc t2, nil, _, ::-::-similar p _ => (0, 0, 0, 0, homogen-zro, homogen-zro, p *> simplify)
| 0, 0, suc t2, c1 :: l1, _, ::-::-similar p q => (c1, 0, n1, 0, l1h 0, homogen-zro, p *> simplify)
| 0, suc t1, 0, _, nil, ::-::-similar p q => (0, 0, 0, 0, homogen-zro, homogen-zro, p *> simplify)
| 0, suc t1, 0, _, c2 :: l2, ::-::-similar p q => (0, c2, 0, n2, homogen-zro, l2h 0, p *> simplify)
| 0, suc t1, suc t2, l1, l2, ::-::-similar p q => (0, 0, 0, 0, homogen-zro, homogen-zro, p *> simplify)
| suc s, 0, 0, nil, nil, ::-nil-similar _ q => aux s 0 0 n1 n2 l1h l2h q
| suc s, 0, 0, nil, c2 :: l2, ::-::-similar _ q => aux s 0 0 n1 (suc n2) l1h (\lam j => l2h (suc j)) q
| suc s, 0, 0, c1 :: l1, nil, ::-::-similar _ q => aux s 0 0 (suc n1) n2 (\lam j => l1h (suc j)) l2h (rewrite sum_nil q)
| suc s, 0, 0, c1 :: l1, c2 :: l2, ::-::-similar _ q => aux s 0 0 (suc n1) (suc n2) (\lam j => l1h (suc j)) (\lam j => l2h (suc j)) q
| suc s, 0, suc t2, nil, l2, ::-::-similar _ q => aux s 0 t2 n1 n2 l1h l2h q
| suc s, 0, suc t2, c1 :: l1, l2, ::-::-similar _ q => aux s 0 t2 (suc n1) n2 (\lam j => l1h (suc j)) l2h q
| suc s, suc t1, 0, l1, nil, ::-::-similar _ q => aux s t1 0 n1 n2 l1h l2h (rewrite sum_nil q)
| suc s, suc t1, 0, l1, c2 :: l2, ::-::-similar _ q => aux s t1 0 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.2.1
| ret j => ((p j).1, (j, inv $mod_<$ FinJoin-cond _ <∘r id<suc))
| ret_f => unfold $unfold$ unfold \lam s => exts (nat_fin_= $mod_< (FinJoin-cond s.2.1 <∘r id<suc) *> s.2.2, idp) | f_sec j => idp }) *> inv (FinSum-double-dep (\lam i => SigmaFin J \lam j => DecFin (decideEq (p j).1 i)) {\lam s => a s.2.1}) *> FinSum=BigSum {_} {suc$ FinJoin (\lam j => (p j).1)}
\where {
\func array => \new Array E (suc $FinJoin (\lam j => (p j).1)) \lam i => FinSum {_} {SigmaFin J \lam j => DecFin (decideEq (p j).1 i)} (\lam k => a k.1) \lemma array-homogen : isHomogenArray array => \lam n => homogen-FinSum$ later \lam j => transport (isHomogen _) j.2 (p j.1).2
}

\lemma sum-decomp (l : Array (\Sigma E E)) (c : \Pi (i : Fin l.len) -> ∃ (n : Nat) (isHomogen (l i).2 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)).2) n))
(BigSum (map (\lam s => s.1 * s.2) l) = BigSum (\lam n => FinSum (\lam j => (f n).2 j * (l ((f n).4 j)).2)))
=> \let | (inP c') => FinSet.finiteAC c
| (inP d) => FinSet.finiteAC (\lam i => homogen-decomp (l i).1)
| p k : _ => later \$ (k.2 Nat.+ (c' k.1).1, homogen-* ((d k.1).2 k.2) (c' k.1).2)
| q => path (\lam i => BigSum (\lam i' => inv (FinSum=BigSum *> (d i').3) i * (l i').2)) *> inv FinSum=BigSum *>
pmap FinSum (ext \lam j => FinSum-rdistr) *> FinSum-double-dep (\lam i => FinFin (DArray.len {(d i).1})) *> FinSum-homogen p
\in inP (suc _, \lam n => (SigmaFin (SigmaFin (FinFin l.len) (\lam i => FinFin (DArray.len {(d i).1}))) (\lam k => DecFin (decideEq (p k).1 n)), \lam k => (d k.1.1).1 k.1.2, \lam k => (k.1.2, (d k.1.1).2 k.1.2), __.1.1, \lam k => transport (isHomogen _) k.2 (p k.1).2), 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 = 0) (Similar nil l')
| a :: l, nil => ::-nil-similar (a = 0) (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 = 0 \elim l, s, j
| a :: l, ::-nil-similar p s, 0 => 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 = 0) \elim l, l', s, j
| a :: l, nil, ::-nil-similar p s, 0 => inr p
| a :: l, nil, ::-nil-similar p s, suc j => \case similar-eq s j \with {
| inl r => \case r.1
| inr r => inr r
}
| a :: l, a' :: l', ::-::-similar p s, 0 => inl (0, p, idp)
| a :: l, a' :: l', ::-::-similar p s, suc j => \case similar-eq s j \with {
| inl r => inl (suc r.1, r.2, pmap suc r.3)
| inr r => inr r
}
}