tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m  : Nat)
                       (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
       delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d)
tailDelta-to-tail-nt O O f (mono (delta x d)) = refl
tailDelta-to-tail-nt O (S m) f (mono (delta x d)) = refl
tailDelta-to-tail-nt (S n) O f (delta (delta x (mono xx)) d) = begin
  delta (mono (f xx)) (delta-fmap tailDelta (delta-fmap (delta-fmap f) d))
  ≡⟨ cong (\de -> delta (mono (f xx)) de) (tailDelta-to-tail-nt n O f d) ⟩
  delta (mono (f xx)) (delta-fmap (delta-fmap f) (delta-fmap tailDelta d))
  ∎
tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin
  delta (delta (f xx) (delta-fmap f d)) (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))
  ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩
  delta (delta (f xx) (delta-fmap f d)) (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))
  ∎

delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n))
               -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d)
delta-mu-is-nt {n = O} f (mono d) = refl
delta-mu-is-nt {n = S n} f (delta (delta x d) ds) = begin
  delta (f x) (delta-mu (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)))
  ≡⟨ cong (\de -> delta (f x) (delta-mu de)) (tailDelta-to-tail-nt n n f ds ) ⟩
  delta (f x) (delta-mu (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)))
  ≡⟨ cong (\de -> delta (f x) de) (delta-mu-is-nt f (delta-fmap tailDelta ds)) ⟩
  delta (f x) (delta-fmap f (delta-mu (delta-fmap tailDelta ds)))
  ∎