{α : Type u_1} →
  {β : Type u_2} →
    {σ : Type u_3} →
      [DecidableEq α] →
        [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
          [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] →
            [Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] →
              σ → List (Std.Tactic.BVDecide.LRAT.Action β α) → Std.Tactic.BVDecide.LRAT.Internal.Result