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 0 = 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 0)  μ (g 0)
  mbs-bad-sub-⊑-minimal-zero = mbs-helper-minimal 0

  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 0  k (r 0)

    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 0 in eq
      ... | zero = ¬¬-elim not-g-bad
        where
        not-g-bad : ¬ ¬ Good _≼_ g
        not-g-bad g-bad = ≤⇒≯ h≤ h>
          where
          h≤ : μ (mbs 0)  μ (g 0)
          h≤ = mbs-bad-sub-⊑-minimal-zero g 
                (g-bad , 
                 Sub-⊑-transitive _⊑_ ⊑-transitive {f} {mbs} {g} 
                    (proj₂ mbs-bad-sub-⊑-member) 
                    g∈Sub-⊑)
          h> : μ (g 0) < μ (mbs 0)
          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 0
        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 0 (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 0

    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 0))
```