module Quox.OPE.Sub

import Quox.OPE.Basics
import Quox.OPE.Length
import Quox.NatExtra
import Data.DPair
import Data.SnocList.Elem
import Data.SnocList.Quantifiers

%default total

infix 0 `Sub'`, `Sub`

public export
data Sub' : Scope a -> Scope a -> Type where
  End  : [<] `Sub'` [<]
  Keep : xs `Sub'` ys -> xs :< z `Sub'` ys :< z
  Drop : xs `Sub'` ys -> xs      `Sub'` ys :< z
%name Sub' p, q

export
keepInjective : Keep p = Keep q -> p = q
keepInjective Refl = Refl

export
dropInjective : Drop p = Drop q -> p = q
dropInjective Refl = Refl

-- these need to be `public export` so that
-- `id`, `zero`, and maybe others can reduce
public export %hint
lengthLeft : xs `Sub'` ys -> Length xs
lengthLeft End      = Z
lengthLeft (Keep p) = S (lengthLeft p)
lengthLeft (Drop p) = lengthLeft p

public export %hint
lengthRight : xs `Sub'` ys -> Length ys
lengthRight End      = Z
lengthRight (Keep p) = S (lengthRight p)
lengthRight (Drop p) = S (lengthRight p)


export %inline
dropLast' : (xs :< x) `Sub'` ys -> xs `Sub'` ys
dropLast' (Keep p) = Drop p
dropLast' (Drop p) = Drop $ dropLast' p

export
Uninhabited (xs :< x `Sub'` [<]) where uninhabited _ impossible

export
Uninhabited (xs :< x `Sub'` xs) where
  uninhabited (Keep p) = uninhabited p
  uninhabited (Drop p) = uninhabited $ dropLast' p


export
0 lteLen : xs `Sub'` ys -> length xs `LTE` length ys
lteLen End      = LTEZero
lteLen (Keep p) = LTESucc $ lteLen p
lteLen (Drop p) = lteSuccRight $ lteLen p

export
0 lteNilRight : xs `Sub'` [<] -> xs = [<]
lteNilRight End = Refl



public export
refl' : Length xs => xs `Sub'` xs
refl' @{Z}   = End
refl' @{S s} = Keep refl'

public export
zero' : Length xs => [<] `Sub'` xs
zero' @{Z}   = End
zero' @{S s} = Drop zero'

public export
single' : Length xs => x `Elem` xs -> [< x] `Sub'` xs
single' @{S _} Here      = Keep zero'
single' @{S _} (There p) = Drop $ single' p


namespace Sub
  public export
  (.) : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
  End      . End      = End
  (Keep p) . (Keep q) = Keep $ p . q
  (Keep p) . (Drop q) = Drop $ p . q
  (Drop p) . q        = Drop $ p . q

public export
comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
comp' = (.)

public export %inline
trans' : xs `Sub'` ys -> ys `Sub'` zs -> xs `Sub'` zs
trans' = flip (.)

public export
app' : xs1 `Sub'` ys1 -> xs2 `Sub'` ys2 -> (xs1 ++ xs2) `Sub'` (ys1 ++ ys2)
app' p End      = p
app' p (Keep q) = Keep $ app' p q
app' p (Drop q) = Drop $ app' p q


||| if `p` holds for all elements of the main list,
||| it holds for all elements of the sublist
public export
subAll' : xs `Sub'` ys -> All p ys -> All p xs
subAll' End      [<]       = [<]
subAll' (Keep q) (ps :< x) = subAll' q ps :< x
subAll' (Drop q) (ps :< x) = subAll' q ps

||| if `p` holds for one element of the sublist,
||| it holds for one element of the main list
public export
subAny' : xs `Sub'` ys -> Any p xs -> Any p ys
subAny' (Keep q) (Here  x) = Here x
subAny' (Keep q) (There x) = There (subAny' q x)
subAny' (Drop q) x         = There (subAny' q x)


public export
data SubView : (lte : xs `Sub'` ys) -> (mask : Nat) -> Type where
  [search lte]
  END  : (0 eq : n = 0) -> SubView End n
  KEEP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
         (0 v : SubView p n) -> (0 eq : n' = S (2 * n)) ->
         SubView (Keep {z} p) n'
  DROP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
         (0 v : SubView p n) -> (0 eq : n' = 2 * n) ->
         SubView (Drop {z} p) n'
%name SubView v

public export
record Sub {a : Type} (xs, ys : Scope a) where
  constructor SubM
  mask : Nat
  0 lte : xs `Sub'` ys
  0 view0 : SubView lte mask
%name Sub sub

public export %inline
sub : {mask : Nat} -> {0 lte : xs `Sub'` ys} -> (0 view0 : SubView lte mask) ->
      xs `Sub` ys
sub v = SubM _ _ v


private
0 uip : (p, q : a = b) -> p = q
uip Refl Refl = Refl

export
0 viewIrrel : Length ys =>
              {m : Nat} -> {lte : xs `Sub'` ys} ->
              (v1, v2 : SubView lte m) -> v1 === v2
viewIrrel (END eq1) (END eq2) = rewrite uip eq1 eq2 in Refl
viewIrrel (KEEP v1 eq1) (KEEP v2 eq2) with (sDoubleInj $ trans (sym eq1) eq2)
  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
viewIrrel (DROP v1 eq1) (DROP v2 eq2) with (doubleInj $ trans (sym eq1) eq2)
  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl

export
0 viewLteEq : {p, q : xs `Sub'` ys} -> SubView p m -> SubView q m -> p = q
viewLteEq (END _) (END _) = Refl
viewLteEq (KEEP {n = m} pv pe) (KEEP {n} qv qe) =
  let eq = sDoubleInj {m, n} $ trans (sym pe) qe in
  rewrite viewLteEq pv (rewrite eq in qv) in Refl
viewLteEq (KEEP pv pe) (DROP qv qe) = absurd $ lsbMutex qe pe
viewLteEq (DROP pv pe) (KEEP qv qe) = absurd $ lsbMutex pe qe
viewLteEq (DROP {n = m} pv pe) (DROP {n} qv qe) =
  let eq = doubleInj {m, n} $ trans (sym pe) qe in
  rewrite viewLteEq pv (rewrite eq in qv) in Refl

private
0 lteEq' : (p : xs `Sub'` ys) ->
           (v1 : SubView p m1) -> (v2 : SubView p m2) ->
           SubM m1 p v1 = SubM m2 p v2
lteEq' End (END Refl) (END Refl) = Refl
lteEq' {m1 = S (2 * n)} {m2 = S (2 * n)} (Keep p) (KEEP v1 Refl) (KEEP v2 Refl) =
  cong (\v => SubM (S (2 * n)) (Keep p) (KEEP v Refl)) $
    case lteEq' p v1 v2 of Refl => Refl
lteEq' {m1 = 2 * n} {m2 = 2 * n} (Drop p) (DROP v1 Refl) (DROP v2 Refl) =
  cong (\v => SubM (2 * n) (Drop p) (DROP v Refl)) $
    case lteEq' p v1 v2 of Refl => Refl
lteEq' {m1 = _} {m2 = S _} _ _ (END _) impossible
lteEq' {m1 = Z} {m2 = _} _ (KEEP _ _) _ impossible
lteEq' {m1 = _} {m2 = Z} _ _ (KEEP _ _) impossible

export
0 lteEq : {p, q : xs `Sub` ys} -> p.lte = q.lte -> p = q
lteEq {p = SubM pm pl pv} {q = SubM qm ql qv} eq =
  rewrite eq in lteEq' ql (rewrite sym eq in pv) qv


public export %inline
end : [<] `Sub` [<]
end = SubM 0 End (END Refl)

public export %inline
keep : xs `Sub` ys -> xs :< z `Sub` ys :< z
keep (SubM mask lte view0) = SubM (S (2 * mask)) (Keep lte) (KEEP view0 Refl)

public export %inline
drop : xs `Sub` ys -> xs `Sub` ys :< z
drop (SubM mask lte view0) = SubM (2 * mask) (Drop lte) (DROP view0 Refl)


export
0 keepLte : (p : xs `Sub` ys) -> (keep p).lte = Keep p.lte
keepLte (SubM mask lte view0) = Refl

export
0 dropLte : (p : xs `Sub` ys) -> (drop p).lte = Drop p.lte
dropLte (SubM mask lte view0) = Refl


public export
data Eqv : {xs, ys : Scope a} -> (p, q : xs `Sub` ys) -> Type where
  EQV : {0 p, q : xs `Sub` ys} -> p.mask = q.mask -> p `Eqv` q
%name Eqv eqv

export
Reflexive (xs `Sub` ys) Eqv where
  reflexive = EQV Refl

export
Symmetric (xs `Sub` ys) Eqv where
  symmetric (EQV eq) = EQV $ sym eq

export
Transitive (xs `Sub` ys) Eqv where
  transitive (EQV eq1) (EQV eq2) = EQV $ trans eq1 eq2

export
0 eqvToEq : {p, q : xs `Sub` ys} -> p `Eqv` q -> p = q
eqvToEq {p = SubM _ _ pv} {q = SubM _ _ qv} (EQV Refl) with (viewLteEq pv qv)
  _ | Refl = rewrite viewIrrel pv qv in Refl

export
0 eqToEqv : {p, q : xs `Sub` ys} -> p = q -> p `Eqv` q
eqToEqv Refl = reflexive


export
getMask : SubView lte mask -> Subset Nat (Equal mask)
getMask (END Refl)  = Element 0 Refl
getMask (KEEP v eq) = Element _ eq
getMask (DROP v eq) = Element _ eq


private
splitExEq : {0 f, g : a -> b} ->
            (0 p : (x : a ** f x = g x)) -> Exists (\x => f x = g x)
splitExEq p = Evidence p.fst (irr p.snd)
  where irr : forall a, b. (0 eq : a = b) -> a = b
        irr Refl = Refl

private
0 lteNil2End : (p : [<] `Sub'` [<]) -> p = End
lteNil2End End = Refl

private
0 ltemEnd : SubView p n -> p = End -> n = 0
ltemEnd (END eq) Refl = eq

private
0 ltemEvenDrop : {p : xs `Sub'` (ys :< y)} ->
                 n = 2 * n' -> SubView p n -> (q ** p = Drop q)
ltemEvenDrop eq (KEEP _ eq') = absurd $ lsbMutex eq eq'
ltemEvenDrop eq (DROP {})    = (_ ** Refl)

private
0 fromDROP : {lte : xs `Sub'` ys :< z} -> n = 2 * n' -> lte = Drop lte' ->
             SubView lte n -> SubView lte' n'
fromDROP eq Refl (DROP {n} p Refl) =
  let eq = doubleInj eq {m = n, n = n'} in
  rewrite sym eq in p

private
0 ltemOddKeep : {p : (xs :< x) `Sub'` (ys :< x)} -> {n' : Nat} ->
                n = S (2 * n') -> SubView p n -> (q ** p = Keep q)
ltemOddKeep eq (KEEP {})    = (_ ** Refl)
ltemOddKeep eq (DROP _ eq') = absurd $ lsbMutex eq' eq
ltemOddKeep eq (END _) impossible

private
0 ltemOddLeft : {0 n, n' : Nat} -> {lte : xs `Sub'` ys :< z} ->
                n = S (2 * n') -> SubView lte n ->
                (xs' ** xs = xs' :< z)
ltemOddLeft eq {lte = Keep p} _ = (_ ** Refl)
ltemOddLeft eq {lte = Drop p} (DROP n' eq') = void $ lsbMutex eq' eq

private
0 fromKEEP : {lte : xs :< z `Sub'` ys :< z} ->
             n = S (2 * n') -> lte = Keep lte' ->
             SubView lte n -> SubView lte' n'
fromKEEP eq Refl (KEEP {n} p Refl) =
  let eq = sDoubleInj eq {m = n, n = n'} in
  rewrite sym eq in p


export
view : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
view @{Z} (SubM mask lte view0) with 0 (lteNilRight lte)
  _ | Refl =
    rewrite lteNil2End lte in
    rewrite ltemEnd view0 (lteNil2End lte) in
    END Refl
view @{S sy} (SubM mask lte view0) {ys = ys :< z} with (viewLsb mask)
  _ | Lsb0 n eqn with (splitExEq $ ltemEvenDrop eqn view0)
    _ | Evidence lte' eql =
      rewrite eqn in rewrite eql in
      DROP (fromDROP eqn eql view0) Refl
  _ | Lsb1 n eqn with (splitExEq $ ltemOddLeft eqn view0)
    _ | Evidence xs' Refl =
      let Evidence q eqq = splitExEq $ ltemOddKeep eqn view0 in
      rewrite eqn in rewrite eqq in
      KEEP (fromKEEP eqn eqq view0) Refl

public export %inline
(.view) : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
(.view) = view

public export %inline
review : Length ys => {m : Nat} -> {0 lte : xs `Sub'` ys} ->
         (0 _ : SubView lte m) -> SubView lte m
review v = view $ sub v



export
ltemLen : (sy : Length ys) => xs `Sub` ys -> length xs `LTE` sy.nat
ltemLen (SubM mask lte view0) {sy} with (review view0)
  ltemLen (SubM _ _ _)            | END eq    = LTEZero
  ltemLen (SubM _ _ _) {sy = S _} | KEEP v eq = LTESucc $ ltemLen $ sub v
  ltemLen (SubM _ _ _) {sy = S _} | DROP v eq = lteSuccRight $ ltemLen $ sub v

export
ltemNilRight : xs `Sub` [<] -> xs = [<]
ltemNilRight m = irrelevantEq $ lteNilRight m.lte


export %inline
dropLast : Length ys => (xs :< x) `Sub` ys -> xs `Sub` ys
dropLast (SubM _ _ view0) @{sy} with (review view0)
  dropLast (SubM _ _ _)        | KEEP v _ = drop $ sub v
  dropLast (SubM _ _ _) @{S _} | DROP v _ = drop $ dropLast $ sub v


export
Uninhabited (xs :< x `Sub` [<]) where
  uninhabited sub = void $ uninhabited sub.lte

export
Length xs => Uninhabited (xs :< x `Sub` xs) where
  uninhabited (SubM _ _ view0) @{sx} with (review view0)
    uninhabited (SubM _ _ _) @{S _} | KEEP v _ = uninhabited $ sub v
    uninhabited (SubM _ _ _) @{S _} | DROP v _ = uninhabited $ dropLast $ sub v


export
refl : Length xs => xs `Sub` xs
refl @{Z}   = end
refl @{S s} = keep refl

export
0 reflLte : {sx : Length xs} -> (refl @{sx}).lte = refl' @{sx}
reflLte {sx = Z}   = Refl
reflLte {sx = S s} = trans (keepLte _) $ cong Keep reflLte

public export %inline
Reflexive (Scope a) Sub where reflexive = refl

mutual
  private
  antisym_ : Length xs => Length ys =>
             {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` xs} ->
             SubView p m1 -> SubView q m2 -> xs = ys
  antisym_ (END _)  (END _) = Refl
  antisym_ (KEEP v1 _) (KEEP v2 _ {z}) @{S sx} @{S sy} =
    cong (:< z) $ antisym (SubM _ _ v1) (SubM _ _ v2)
  antisym_ (KEEP {}) (DROP {}) {p = Keep p} {q = Drop q} =
    void $ succNotLTEpred $ lteLen q `transitive` lteLen p
  antisym_ (DROP {}) (KEEP {}) {p = Drop p} {q = Keep q} =
    void $ succNotLTEpred $ lteLen p `transitive` lteLen q
  antisym_ (DROP {}) (DROP {}) {p = Drop p} {q = Drop q} =
    void $ succNotLTEpred $ lteLen p `transitive` lteSuccLeft (lteLen q)

  export
  antisym : Length xs => Length ys => xs `Sub` ys -> ys `Sub` xs -> xs = ys
  antisym v1 v2 = antisym_ v1.view v2.view

public export %inline
Antisymmetric (Scope a) Sub where
  antisymmetric p q = antisym p q


mutual
  private
  trans_ : Length ys => Length zs =>
           {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` zs} ->
           SubView p m1 -> SubView q m2 -> xs `Sub` zs
  trans_ (END _) (END _) = end
  trans_ (KEEP v1 _) (KEEP v2 _) @{S sy} @{S sz} = keep $ sub v1 `trans` sub v2
  trans_ (DROP v1 _) (KEEP v2 _) @{S sy} @{S sz} = drop $ sub v1 `trans` sub v2
  trans_ v1 (DROP v2 _) @{sy} @{S sz} =
    let Element m1' eq = getMask v1 in
    drop $ SubM m1' _ (rewrite sym eq in v1) `trans` sub v2

  export
  trans : Length ys => Length zs => xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
  trans p q = trans_ p.view q.view

public export %inline
(.) : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
(.) = flip trans

public export %inline
comp : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
comp = (.)

public export %inline
Transitive (Scope a) Sub where
  transitive p q = q . p


public export
zero : Length xs => [<] `Sub` xs
zero @{Z}   = end
zero @{S s} = drop zero

export
0 zeroLte : {sx : Length xs} -> (zero @{sx}).lte = zero' @{sx}
zeroLte {sx = Z}   = Refl
zeroLte {sx = S s} = trans (dropLte zero) $ cong Drop zeroLte

public export
single : Length xs => x `Elem` xs -> [< x] `Sub` xs
single @{S sx} Here      = keep zero
single @{S sx} (There p) = drop $ single p

export
0 singleLte : {sx : Length xs} -> (p : x `Elem` xs) ->
              (single p @{sx}).lte = single' p @{sx}
singleLte {sx = S s} Here      = trans (keepLte zero) $ cong Keep zeroLte
singleLte {sx = S s} (There p) = trans (dropLte _) $ cong Drop $ singleLte p


mutual
  private
  app0 : Length ys2 =>
         (l : xs1 `Sub` ys1) ->
         {rm : Nat} -> {0 rl : xs2 `Sub'` ys2} -> (rv : SubView rl rm) ->
         (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
  app0 l (END eq)              = l
  app0 l (KEEP v Refl) @{S sy} = keep $ l ++ sub v
  app0 l (DROP v Refl) @{S sy} = drop $ l ++ sub v

  export
  app : Length ys2 =>
        xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
  app l r = app0 l r.view

  public export %inline
  (++) : Length ys2 =>
         xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
  (++) = app

export
0 appLte : {sy : Length ys2} ->
           (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
           (app l r @{sy}).lte = app' l.lte r.lte
appLte l r@(SubM 0 End (END Refl)) =
  cong (\v => (app0 l v).lte) (viewIrrel (view end) (END Refl))
appLte l r@(SubM (S (2 * n)) (Keep p) (KEEP v Refl)) {sy = S sy} =
  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (KEEP v Refl))) $
  trans (keepLte _) $
  cong Keep $ appLte l (sub v)
appLte l r@(SubM 0 (Drop p) (DROP {n = 0} v Refl)) {sy = S sy} =
  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
  trans (dropLte _) $
  cong Drop $ appLte l (sub v)
appLte l r@(SubM (2 * S n) (Drop p) (DROP {n = S n} v Refl)) {sy = S sy} =
  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
  trans (dropLte _) $
  cong Drop $ appLte l (sub v)
appLte {xs2 = _ :< _, ys2 = [<]} _ (SubM _ _ _) impossible

export
0 keepAppRight : {sy : Length ys2} ->
                 (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
                 (l ++ keep r) @{S sy} = keep ((l ++ r) @{sy})
keepAppRight l (SubM mask _ _) = rewrite (lsbOdd mask).snd in Refl

export
0 dropAppRight : (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
                 (l ++ drop r) @{S sy} = drop ((l ++ r) @{sy})
dropAppRight l r = lteEq $
  trans (appLte l (drop r)) $
  trans (cong (app' l.lte) (dropLte r)) $
  trans (cong Drop (sym (appLte l r))) $
  sym $ dropLte (l ++ r)


export
0 endRight : {xs, ys : Scope a} -> (sub : xs `Sub` ys) -> sub = (sub ++ Sub.end)
endRight sub = Refl


private
0 transDrop_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
               (pv : SubView p m1) -> (qv : SubView q m2) ->
               trans_ pv (DROP qv qe) @{sy} @{S sz} =
                 drop (trans_ pv qv @{sy} @{sz})
transDrop_ {sy = Z} {sz = sz} (END Refl) qv =
  cong (\v => drop $ trans_ {m2, q} (END Refl) v) $ viewIrrel {}
transDrop_ {sy = S sy} {sz = sz} (KEEP pv Refl) qv {p = Keep p} =
  cong2 (\x, y => drop (trans_ @{S sy} x y)) (viewIrrel {}) (viewIrrel {})
transDrop_ {sy = S sy} {sz = S sz} (DROP pv Refl) qv =
  cong2 (\x, y => drop (trans_ @{S sy} @{S sz} x y))
    (viewIrrel {}) (viewIrrel {})
transDrop_ {ys = _ :< _, zs = [<]} _ _ impossible

private
0 transLte_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
              (pv : SubView p m1) -> (qv : SubView q m2) ->
              (trans_ pv qv @{sy} @{sz}).lte = trans' p q
transLte_ (END _) (END _) = Refl
transLte_ (KEEP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
  trans (keepLte _) $ cong Keep $ transLte_ {}
transLte_ (DROP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
  trans (dropLte _) $ cong Drop $ transLte_ {}
transLte_ pv (DROP qv qe) {sz = S _} =
  trans (cong lte $ transDrop_ pv qv) $
  trans (dropLte _) $ cong Drop $ transLte_ pv qv
transLte_ {ys = _ :< _, zs = [<]} _ _ impossible

export
0 transLte : {sy : Length ys} -> {sz : Length zs} ->
             (p : xs `Sub` ys) -> (q : ys `Sub` zs) ->
             (trans p q @{sy} @{sz}).lte = trans' p.lte q.lte
transLte p q = transLte_ p.view q.view

public export
0 compLte : {sy : Length ys} -> {sz : Length zs} ->
            (q : ys `Sub` zs) -> (p : xs `Sub` ys) ->
            ((q . p) @{sy} @{sz}).lte = q.lte . p.lte 
compLte q p = transLte p q


||| if `p` holds for all elements of the main list,
||| it holds for all elements of the sublist
export
subAll : Length ys => xs `Sub` ys -> All prop ys -> All prop xs
subAll (SubM _ _ v) ps @{sy} with (review v)
  subAll (SubM _ _ _) [<]               | END    _ = [<]
  subAll (SubM _ _ _) (ps :< p) @{S sy} | KEEP v _ = subAll (sub v) ps :< p
  subAll (SubM _ _ _) (ps :< p) @{S sy} | DROP v _ = subAll (sub v) ps


||| if `p` holds for one element of the sublist,
||| it holds for one element of the main list
export
subAny : Length ys => xs `Sub` ys -> Any prop xs -> Any prop ys
subAny (SubM _ _ v) p @{sy} with (review v)
  subAny (SubM _ _ _) (Here  p)         | KEEP v _ = Here p
  subAny (SubM _ _ _) (There p) @{S sy} | KEEP v _ = There $ subAny (sub v) p
  subAny (SubM _ _ _) p         @{S sy} | DROP v _ = There $ subAny (sub v) p