{α₂ γ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m γ) → Sort u_3) →
      (it₂ : Option (Std.IterM m γ)) →
        (it₂ = none → motive none) → ((it₂_1 : Std.IterM m γ) → it₂ = some it₂_1 → motive (some it₂_1)) → motive it₂