The minimal bad sequence argument, slightly generalized.

```agda
module MinimalBadSeq where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; cong; cong-app; subst)
-- open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _∸_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
  -- Don't use the library version of ≤-<-connex.
  using (≤-reflexive; ≤-refl; ≤-trans; <-trans; <-irrefl; <⇒≤; <-transʳ; ≤⇒≯; n∸n≡0; ∸-monoˡ-<)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_)
open import Function using (_∘_; id)

open import Miscellaneous

open import Classical

open import WQO
```

"Induction step" of the construction of MBS.
```agda
module MinSeqStep {A : Set} (μ : A → ℕ) (P : (ℕ → A) → Set) (P-nonempty : NonEmpty P) where
  μP : (ℕ → ℕ) → Set
  μP = (μ ∘_) [ P ]  -- μP g = Σ[ f ∈ (ℕ → A) ] (f ∈ P × μ ∘ f ≡ g)

  μP-nonempty : NonEmpty μP
  μP-nonempty = nonempty-image (μ ∘_) P P-nonempty

  record MinSeqAt (n : ℕ) : Set where
    field
      seq : ℕ → A
      member : seq ∈ P
      minimal : (g : ℕ → A) → g ∈ P → μ (seq n) ≤ μ (g n)

  minSeqAt : (n : ℕ) → MinSeqAt n
  minSeqAt n =
    record
    { seq = f
    ; member   = f∈P
    ; minimal  = f-minimal
    }
    where
    lμP : Σ[ f₁ ∈ (ℕ → ℕ) ] (f₁ ∈ μP × ((g₁ : ℕ → ℕ) → g₁ ∈ μP → f₁ n ≤ g₁ n))
    lμP = leastSeqAt μP-nonempty n
    f₁ = proj₁ lμP
    f₁∈μP = proj₁ (proj₂ lμP)
    f = proj₁ f₁∈μP
    f∈P : f ∈ P
    f∈P = proj₁ (proj₂ f₁∈μP)
    μ∘f≡f₁ : μ ∘ f ≡ f₁
    μ∘f≡f₁ = proj₂ (proj₂ f₁∈μP)
    f₁-minimal : (g₁ : ℕ → ℕ) → g₁ ∈ μP → f₁ n ≤ g₁ n
    f₁-minimal = proj₂ (proj₂ lμP)
    f-minimal : (g : ℕ → A) → g ∈ P → μ (f n) ≤ μ (g n)
    f-minimal g g∈P rewrite cong-app μ∘f≡f₁ n = f₁-minimal g₁ g₁∈μP
      where
      g₁ = μ ∘ g
      g₁∈μP : g₁ ∈ μP
      g₁∈μP = member-image (μ ∘_) P g∈P
```

The constructon of the minimal "bad" sequence is relativized to the predicate P.
We construct the minimal sequence with respect to P, which is known to be nonempty.
```agda
module MBS-helper {A : Set} (μ : A → ℕ) (P : (ℕ → A) → Set) (P-nonempty : NonEmpty P) where
  open MinSeqStep {A} μ

  P′ : ℕ → (ℕ → A) → Set
  P′-nonempty : (n : ℕ) → NonEmpty (P′ n)
  mbs-helper : (n : ℕ) → MinSeqAt (P′ n) (P′-nonempty n) n
      -- Σ[ f ∈ (ℕ → A) ] f ∈ P′ n × ((g : ℕ → A) → g ∈ P′ n → μ (f n) ≤ μ (g n))
  mbs-helper-seq : ℕ → ℕ → A
  mbs-helper-member : (n : ℕ) → mbs-helper-seq n ∈ P

  P′ zero = P
  P′ (suc n) g = g ∈ P × AgreeUpTo n (mbs-helper-seq n) g

  P′-nonempty  = P-nonempty
  P′-nonempty (suc n) = mbs-helper-seq n , mbs-helper-member n , agreeUpTo-reflexive n (mbs-helper-seq n)

  mbs-helper n = minSeqAt (P′ n) (P′-nonempty n) n

  mbs-helper-seq n = MinSeqAt.seq (mbs-helper n)
  mbs-helper-member zero = MinSeqAt.member (mbs-helper zero)
  mbs-helper-member (suc n) = proj₁ (MinSeqAt.member (mbs-helper (suc n)))

  mbs-helper-minimal : (n : ℕ) (g : ℕ → A) → g ∈ P′ n → μ (mbs-helper-seq n n) ≤ μ (g n)
  mbs-helper-minimal n = MinSeqAt.minimal (mbs-helper n)

  mbs-helper-agreeUpTo : (m n : ℕ) → m ≤ n → AgreeUpTo m (mbs-helper-seq m) (mbs-helper-seq n)
  mbs-helper-agreeUpTo .zero zero z≤n = agreeUpTo-reflexive zero (mbs-helper-seq zero)
  mbs-helper-agreeUpTo m (suc n) m≤1+n with ≤-suc m≤1+n
  ... | inj₁ m≤n = agreeUpTo-transitive (mbs-helper-agreeUpTo m n m≤n)
                    (agreeUpTo-≤ (mbs-helper-agreeUpTo-step n) m≤n)
    where
    mbs-helper-agreeUpTo-step : (n : ℕ)
      → AgreeUpTo n (mbs-helper-seq n) (mbs-helper-seq (suc n))
    mbs-helper-agreeUpTo-step n = proj₂ (MinSeqAt.member (mbs-helper (suc n)))
  ... | inj₂ refl = agreeUpTo-reflexive (suc n) (mbs-helper-seq (suc n))

  mbs : ℕ → A
  mbs n = mbs-helper-seq n n
```

In general, the minimal sequence relativized to P need not itself satisfy P.
We need the condition we call "initial segment property" for the mbs to satisfy P.
```agda
  module _ (P-isp : InitialSegmentProperty P) where

    mbs-member : mbs ∈ P
    mbs-member = P-isp mbs (λ (n : ℕ) → 
                              mbs-helper-seq n , 
                              mbs-helper-member n , 
                              λ {m : ℕ} (m≤n : m ≤ n) → mbs-helper-agreeUpTo m n m≤n ≤-refl)
```

The predicate "bad" is closed under subsequence, as well as satisfying the initial segment property.
```
module _ {A : Set} (_≼_ : A → A → Set) where
  Bad = ¬_ ∘ (Good _≼_)

  subseq-bad : {f : ℕ → A} → Bad f → (r : ℕ → ℕ) → Increasing _<_ r → Bad (f ∘ r)
  subseq-bad {f} f-bad r r-increasing (i , j , i<j , fri≼frj) = 
    f-bad (r i , r j , r-increasing i j i<j , fri≼frj)

  Bad-isp : InitialSegmentProperty {A} Bad
  Bad-isp f h f-good = contra
    where
    i j : ℕ
    i = proj₁ f-good
    j = proj₁ (proj₂ f-good)
    i<j : i < j
    i<j = proj₁ (proj₂ (proj₂ f-good))
    fi≼fj : f i ≼ f j
    fi≼fj = proj₂ (proj₂ (proj₂ f-good))
    g : ℕ → A
    g = proj₁ (h j)
    g-bad : Bad g
    g-bad = proj₁ (proj₂ (h j))
    h₁ : AgreeUpTo j f g
    h₁ = proj₂ (proj₂ (h j))
    fi≡gi : f i ≡ g i
    fi≡gi = h₁ (<⇒≤ i<j)
    fj≡gj : f j ≡ g j
    fj≡gj = h₁ ≤-refl
    gi≼gj : g i ≼ g j
    gi≼gj rewrite sym fi≡gi | sym fj≡gj = fi≼fj
    contra : ⊥
    contra = g-bad (i , j , i<j , gi≼gj)
```

We restrict attention to sequences that can be obtained from a subsequence of a given sequence f by 
taking a "substructure" of each term in the subsequence.
This predicate satisfies the initial segment property.
```
module _ {A : Set} (_⊑_ : A → A → Set) where

  Sub-⊑ : (ℕ → A) → (ℕ → A) → Set
  Sub-⊑ f g = Σ[ r ∈ (ℕ → ℕ) ] Increasing _<_ r × ((n : ℕ) → g n ⊑ f (r n) )

  Sub-⊑-isp : (f : ℕ → A) → InitialSegmentProperty (Sub-⊑ f)
  Sub-⊑-isp f g h = r , r-increasing , r-witness
    where
    S : ℕ → (ℕ → ℕ) → Set
    S n s = Increasing _<_ s × ((m : ℕ) → m ≤ n → g m ⊑ f (s m))
    S-nonempty : (n : ℕ) → NonEmpty (S n)
    S-nonempty n = s₁ , s₁-increasing , h₃
      where
      g₁ : ℕ → A
      g₁ = proj₁ (h n)
      g₁∈Sub-⊑f : g₁ ∈ Sub-⊑ f
      g₁∈Sub-⊑f = proj₁ (proj₂ (h n))
      s₁ : ℕ → ℕ
      s₁ = proj₁ g₁∈Sub-⊑f
      s₁-increasing : Increasing _<_ s₁
      s₁-increasing = proj₁ (proj₂ g₁∈Sub-⊑f)
      h₁ : (m : ℕ) → g₁ m ⊑ f (s₁ m)
      h₁ = proj₂ (proj₂ g₁∈Sub-⊑f)
      h₂ : AgreeUpTo n g g₁
      h₂ = proj₂ (proj₂ (h n))
      h₃ : (m : ℕ) → m ≤ n → g m ⊑ f (s₁ m)
      h₃ m m≤n rewrite h₂ m≤n = h₁ m
    minS : (n : ℕ) → Σ[ s ∈ (ℕ → ℕ) ] (s ∈ S n × ((s′ : ℕ → ℕ) → s′ ∈ S n → s n ≤ s′ n))
    minS n = leastSeqAt (S-nonempty n) n
    t : ℕ → ℕ → ℕ
    t n = proj₁ (minS n)
    tn∈Sn : (n : ℕ) → t n ∈ S n
    tn∈Sn n = proj₁ (proj₂ (minS n))
    tn-increasing : (n : ℕ) → Increasing _<_ (t n)
    tn-increasing n = proj₁ (tn∈Sn n)
    tn-witness : (n m : ℕ) → m ≤ n → g m ⊑ f (t n m)
    tn-witness n = proj₂ (tn∈Sn n)
    m<n⇒tn∈Sm : (n m : ℕ) → m < n → t n ∈ S m
    m<n⇒tn∈Sm n m m<n = tn-increasing n , λ m₁ m₁≤m → proj₂ (tn∈Sn n) m₁ (≤-trans m₁≤m (<⇒≤ m<n))
    r : ℕ → ℕ
    r n = t n n
    r-increasing : Increasing _<_ r
    r-increasing m n m<n = <-transʳ tmm≤tnm tnm<tnn
      where
      tmm≤tnm : t m m ≤ t n m
      tmm≤tnm = proj₂ (proj₂ (minS m)) (t n) (m<n⇒tn∈Sm n m m<n)
      tnm<tnn : t n m < t n n
      tnm<tnn = tn-increasing n m n m<n
    r-witness : (n : ℕ) → g n ⊑ f (r n)
    r-witness n = tn-witness n n ≤-refl

  Sub-⊑-reflexive : Reflexive _⊑_ → (f : ℕ → A) → f ∈ Sub-⊑ f
  Sub-⊑-reflexive ⊑-reflexive f = id , id-increasing , λ n → ⊑-reflexive

  Sub-⊑-transitive : Transitive _⊑_ → {f g k : ℕ → A}
    → g ∈ Sub-⊑ f
    → k ∈ Sub-⊑ g
    -------------
    → k ∈ Sub-⊑ f
  Sub-⊑-transitive ⊑-transitive (r₁ , r₁-increasing , h₁) (r₂ , r₂-increasing , h₂) = 
    r₁ ∘ r₂ , 
    subseq-increasing _<_ r₁ r₂ r₁-increasing r₂-increasing , 
    λ n → ⊑-transitive (h₂ n) (h₁ (r₂ n))

Sub-⊑-mono : {A : Set} (_⊑₁_ _⊑₂_ : A → A → Set) (f : ℕ → A)
  → ((x y : A) → x ⊑₁ y → x ⊑₂ y)
  → (g : ℕ → A)
  → g ∈ Sub-⊑ _⊑₁_ f
  ------------------
  → g ∈ Sub-⊑ _⊑₂_ f
Sub-⊑-mono _⊑₁_ _⊑₂_ f ⊑₁⇒⊑₂ g (r , r-increasing , h) = 
  r , r-increasing , λ n → ⊑₁⇒⊑₂ (g n) (f (r n)) (h n)
```

The predicate we use is the conjunction of "bad" and the above predicate.
So, given a bad sequence f, we construct the minimal bad sequence that can be obtained from 
a subsequence of f by taking substructures.
```agda
module MBS {A : Set} (μ : A → ℕ) (_≼_ : A → A → Set) 
        (_⊑_ : A → A → Set) (⊑-reflexive : Reflexive _⊑_)
        {f : ℕ → A} (f-bad : ¬ Good _≼_ f) where

  Bad-Sub-⊑ : (ℕ → A) → Set
  Bad-Sub-⊑ = λ (g : ℕ → A) → ¬ Good _≼_ g × Sub-⊑ _⊑_ f g

  Bad-Sub-⊑-nonempty : NonEmpty Bad-Sub-⊑
  Bad-Sub-⊑-nonempty = f , f-bad , Sub-⊑-reflexive _⊑_ ⊑-reflexive f

  open MBS-helper {A} μ Bad-Sub-⊑ Bad-Sub-⊑-nonempty public

  mbs-bad-sub-⊑-member : mbs ∈ Bad-Sub-⊑
  mbs-bad-sub-⊑-member = mbs-member (ISP-closed-∩ (¬_ ∘ (Good _≼_)) (Sub-⊑ _⊑_ f) 
                                (Bad-isp _≼_) (Sub-⊑-isp _⊑_ f))

  mbs-bad : ¬ Good _≼_ mbs
  mbs-bad = proj₁ mbs-bad-sub-⊑-member

  mbs-sub-⊑ : mbs ∈ Sub-⊑ _⊑_ f
  mbs-sub-⊑ = proj₂ mbs-bad-sub-⊑-member

  mbs-bad-sub-⊑-minimal-zero : (g : ℕ → A) → g ∈ Bad-Sub-⊑ → μ (mbs ) ≤ μ (g )
  mbs-bad-sub-⊑-minimal-zero = mbs-helper-minimal 

  mbs-bad-sub-⊑-minimal-suc : (n : ℕ) (g : ℕ → A)
    → g ∈ Bad-Sub-⊑ → AgreeUpTo n mbs g → μ (mbs (suc n)) ≤ μ (g (suc n))
  mbs-bad-sub-⊑-minimal-suc n g h₁ h₂ = mbs-helper-minimal (suc n) g (h₁ , h)
    where
    h : AgreeUpTo n (mbs-helper-seq n) g
    h {m} m≤n = trans (sym (mbs-helper-agreeUpTo m n m≤n ≤-refl)) (h₂ m≤n)
``` 

A general form of the minimal bad sequence argument.
If mbs is the minimal bad sequence (with respect to our predicate), then any sequence that can be
obtained by taking a "proper" substructure of each term of a subsequence of mbs must be good, provided
that the binary relation ≼ in question is "monotone" on the right argument with respect to the substructure
relation ⊑.
```
  _⊏_ : A → A → Set
  x ⊏ y = x ⊑ y × x ≢ y

  ⊏⇒⊑ : (x y : A) → x ⊏ y → x ⊑ y
  ⊏⇒⊑ x y (x⊑y , x≢y) = x⊑y

  module Sub-⊑-⊏
    (⊏-μ-< : {x y : A} → x ⊏ y → μ x < μ y)
    (≼-⊑-≼ : {x y z : A} → x ≼ y → y ⊑ z → x ≼ z)
    (⊑-transitive : Transitive _⊑_)
    where

    ⊏-transitive : {x y z : A} → x ⊏ y → y ⊏ z → x ⊏ z
    ⊏-transitive {x} {y} {z} x⊏y@(x⊑y , x≢y) y⊏z@(y⊑z , y≢z) = 
      ⊑-transitive x⊑y y⊑z , 
      λ x≡z → <-irrefl (cong μ x≡z) (<-trans (⊏-μ-< x⊏y) (⊏-μ-< y⊏z))

    Sub-⊑-⊏-0 : (ℕ → A) → (ℕ → A) → Set
    Sub-⊑-⊏-0 k g = Σ[ r ∈ (ℕ → ℕ) ] Increasing _<_ r × ((n : ℕ) → g n ⊑ k (r n)) × g  ⊏ k (r )

    Sub-⊑-⊏-0⇒Sub-⊑ : (k g : ℕ → A) → Sub-⊑-⊏-0 k g → Sub-⊑ _⊑_ k g
    Sub-⊑-⊏-0⇒Sub-⊑ k g (r , r-increasing , hn , h0) = r , r-increasing , hn

    Sub-⊑-⊏-0-mbs⇒Good : (g : ℕ → A) → g ∈ Sub-⊑-⊏-0 mbs → Good _≼_ g
    Sub-⊑-⊏-0-mbs⇒Good g (r , r-increasing , hn , h0) = g-good
      where
      g∈Sub-⊑ : g ∈ Sub-⊑ _⊑_ mbs
      g∈Sub-⊑ = (r , r-increasing , hn)
      g-good : Good _≼_ g
      g-good with r  in eq
      ... | zero = ¬¬-elim not-g-bad
        where
        not-g-bad : ¬ ¬ Good _≼_ g
        not-g-bad g-bad = ≤⇒≯ h≤ h>
          where
          h≤ : μ (mbs ) ≤ μ (g )
          h≤ = mbs-bad-sub-⊑-minimal-zero g 
                (g-bad , 
                 Sub-⊑-transitive _⊑_ ⊑-transitive {f} {mbs} {g} 
                    (proj₂ mbs-bad-sub-⊑-member) 
                    g∈Sub-⊑)
          h> : μ (g ) < μ (mbs )
          h> = ⊏-μ-< h0
      ... | suc p = i ∸ (suc p) , j ∸ (suc p) , i∸1+p<j∸1+p , gi∸1+p≼gj∸1+p
        where
        g′ = switch′ mbs (λ n → g (n ∸ (suc p))) p
        g′sucp≡g0 : g′ (suc p) ≡ g 
        g′sucp≡g0 rewrite ≤-<-connex-> (suc p) p (s≤s ≤-refl) | n∸n≡0 (suc p) = refl
        r′ = switch′ id (λ n → r (n ∸ (suc p))) p
        r′-≤ : (n : ℕ) → n ≤ p → r′ n ≡ n
        r′-≤ = switch′-≤ id (λ n → r (n ∸ (suc p))) p
        -- r′-> : (n : ℕ) → p < n → r′ n ≡ r (n ∸ (suc p))  -- not used
        -- r′-> = switch′-> id (λ n → r (n ∸ (suc p))) p
        r′-increasing : Increasing _<_ r′
        r′-increasing m n m<n with ≤-<-connex m p | ≤-<-connex n p
        ... | inj₁ m≤p | inj₁ n≤p = m<n
        ... | inj₁ m≤p | inj₂ n>p =
          ≤-trans (s≤s m≤p)
                    (≤-trans (≤-reflexive (sym eq)) 
                             (increasing-≤ r r-increasing  (n ∸ (suc p)) z≤n))
        ... | inj₂ m>p | inj₁ n≤p = ⊥-elim (≤⇒≯ (<⇒≤ (<-transʳ n≤p m>p)) m<n)
        ... | inj₂ m>p | inj₂ n>p =
          r-increasing (m ∸ (suc p)) (n ∸ (suc p)) (∸-monoˡ-< m<n m>p)
        g′-≤ : (n : ℕ) → n ≤ p → g′ n ≡ mbs n
        g′-≤ = switch′-≤ mbs (λ n → g (n ∸ (suc p))) p
        g′-> : (n : ℕ) → p < n → g′ n ≡ g (n ∸ (suc p))
        g′-> = switch′-> mbs (λ n → g (n ∸ suc p)) p
        h₁ : AgreeUpTo p mbs g′
        h₁ = agreeUpTo-symmetric p g′ mbs (λ {n : ℕ} → g′-≤ n)
        h₂ : (n : ℕ) → g′ n ⊑ mbs (r′ n)
        h₂ n with ≤-<-connex n p
        ... | inj₁ n≤p = ⊑-reflexive
        ... | inj₂ n>p = hn (n ∸ (suc p))
        g′∈Sub-⊑ : g′ ∈ Sub-⊑ _⊑_ mbs
        g′∈Sub-⊑ = r′ , r′-increasing , h₂
        not-g′-bad : ¬ ¬ Good _≼_ g′
        not-g′-bad g′-bad = ≤⇒≯ h≤ h>
          where
          h≤ : μ (mbs (suc p)) ≤ μ (g′ (suc p))
          h≤ = mbs-bad-sub-⊑-minimal-suc p g′ 
                (g′-bad , 
                Sub-⊑-transitive _⊑_ ⊑-transitive {f} {mbs} {g′} 
                    (proj₂ mbs-bad-sub-⊑-member) g′∈Sub-⊑)
                h₁
          h> : μ (g′ (suc p)) < μ (mbs (suc p))
          h> rewrite g′sucp≡g0 | eq = ⊏-μ-< h0
        g′-good : Good _≼_ g′
        g′-good = ¬¬-elim not-g′-bad
        i j : ℕ
        i = proj₁ g′-good
        j = proj₁ (proj₂ g′-good)
        i<j : i < j
        i<j = proj₁ (proj₂ (proj₂ g′-good))
        g′i≼g′j : g′ i ≼ g′ j
        g′i≼g′j = proj₂ (proj₂ (proj₂ g′-good))
        p<i : p < i
        p<i = case-⊎ (λ i≤p → ⊥-elim (¬i≤p i≤p)) 
                     (λ i>p → i>p)
                     (≤-<-connex i p)
          where
          ¬i≤p : i ≤ p → ⊥
          ¬i≤p i≤p = 
            mbs-bad (r′ i , r′ j , r′-increasing i j i<j , mbsr′i≼mbsr′j)
            where
            mbsr′i≼mbsr′j : mbs (r′ i) ≼ mbs (r′ j)
            mbsr′i≼mbsr′j = subst (λ z → mbs z ≼ mbs (r′ j)) (sym (r′-≤ i i≤p)) 
                        (subst (_≼ mbs (r′ j)) (g′-≤ i i≤p) (≼-⊑-≼ g′i≼g′j (h₂ j)))
        p<j : p < j
        p<j = <-trans p<i i<j
        gi∸1+p≼gj∸1+p : g (i ∸ (suc p)) ≼ g (j ∸ (suc p))
        gi∸1+p≼gj∸1+p = 
          subst (_≼ g (j ∸ (suc p))) (g′-> i p<i) (subst (g′ i ≼_) (g′-> j p<j) g′i≼g′j)
        i∸1+p<j∸1+p : i ∸ (suc p) < j ∸ (suc p)
        i∸1+p<j∸1+p = ∸-monoˡ-< i<j p<i

    Sub-⊏ : (ℕ → A) → (ℕ → A) → Set
    Sub-⊏ = Sub-⊑ _⊏_

    Sub-⊏⇒Sub-⊑ : (g k : ℕ → A) → k ∈ Sub-⊏ g → k ∈ Sub-⊑ _⊑_ g
    Sub-⊏⇒Sub-⊑ g k h = Sub-⊑-mono _⊏_ _⊑_ g ⊏⇒⊑ k h

    Sub-⊏⇒Sub-⊑-⊏-0 : (g k : ℕ → A) → k ∈ Sub-⊏ g → k ∈ Sub-⊑-⊏-0 g
    Sub-⊏⇒Sub-⊑-⊏-0 g k (r , r-increasing , h) = 
      r , r-increasing , (λ n → ⊏⇒⊑ (k n) (g (r n)) (h n)) , h 

    Sub-⊏-transitive : {d g k : ℕ → A} → g ∈ Sub-⊏ d → k ∈ Sub-⊏ g → k ∈ Sub-⊏ d
    Sub-⊏-transitive {d} {g} {k} = Sub-⊑-transitive _⊏_ ⊏-transitive {d} {g} {k}

    Sub-⊏-mbs⇒VeryGood : (g : ℕ → A) → g ∈ Sub-⊏ mbs → VeryGood _≼_ g
    Sub-⊏-mbs⇒VeryGood g (s , s-increasing , h) r r-increasing = 
      Sub-⊑-⊏-0-mbs⇒Good (g ∘ r) 
        (s ∘ r , 
         subseq-increasing _<_ s r s-increasing r-increasing , 
         (λ n → ⊏⇒⊑ (g (r n)) (mbs (s (r n))) (h (r n))) , 
         h (r ))
```