{ε : Type u_1} →
  {α : Type u_2} →
    {p : α → Prop} →
      (motive : (x? : Except ε α) → SatisfiesM p x? → (∀ (a : α), x? = Except.ok a → p a) → Sort u_3) →
        (x? : Except ε α) →
          (h : SatisfiesM p x?) →
            (h' : ∀ (a : α), x? = Except.ok a → p a) →
              ((x : α) →
                  (h : SatisfiesM p (Except.ok x)) →
                    (h' : ∀ (a : α), Except.ok x = Except.ok a → p a) → motive (Except.ok x) h h') →
                ((e : ε) →
                    (h : SatisfiesM p (Except.error e)) →
                      (h' : ∀ (a : α), Except.error e = Except.ok a → p a) → motive (Except.error e) h h') →
                  motive x? h h'