∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (x : ForInStep γ) (h_1 : (a : γ) → motive (ForInStep.done a))
  (h_2 : (x : ForInStep γ) → motive x),
  (∀ (a : γ), x = ForInStep.done a → False) →
    (match x with
      | ForInStep.done a => h_1 a
      | x => h_2 x) =
      h_2 x