{v : Sat.Valuation} →
  {f : Sat.Fmla} →
    {p : Prop} →
      {motive : Sat.Fmla.reify v f p → Sort u} →
        (t : Sat.Fmla.reify v f p) → ((prop : ¬v.satisfies_fmla f → p) → motive ⋯) → motive t