val remove_index_from_steps_updater
      (u: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
      (tid: tid_t)
      (lsteps: list Armada.Step.t)
      (ls: Armada.State.t)
    : GTot (list Armada.Step.t)
val remove_index_from_steps_updater
      (u: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
      (tid: tid_t)
      (lsteps: list Armada.Step.t)
      (ls: Armada.State.t)
    : GTot (list Armada.Step.t)
let remove_index_from_steps_updater
  (u:(tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
  (tid: tid_t)
  (lsteps: list Armada.Step.t)
  (ls: Armada.State.t)
  : GTot (list Armada.Step.t) =
  let idx, steps = u tid lsteps ls in
  steps
module Strategies.Weakening.Armada

open Armada.Action
open Armada.Base
open Armada.State
open Armada.Step
open Armada.Transition
open Armada.Type
open FStar.List.Tot
open FStar.Tactics.V2
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Weakening
open Spec.List
open Spec.Ubool
open Util.List
/
Util.List.fst.checked Strategies.Weakening.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.Atomic.fsti.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Weakening.Armada.fst

    u166:
      (_: Armada.Base.tid_t -> _: Prims.list Armada.Step.t -> _: Armada.State.t
          -> Prims.GTot (Prims.nat * Prims.list Armada.Step.t)) ->
    tid: Armada.Base.tid_t ->
    lsteps: Prims.list Armada.Step.t ->
    ls: Armada.State.t
  -> Prims.GTot (Prims.list Armada.Step.t)
Armada.Base.tid_t Prims.list Armada.Step.t Armada.State.t FStar.Pervasives.Native.tuple2 Prims.nat
let remove_index_from_steps_updater
      (u: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
      (tid: tid_t)
      (lsteps: list Armada.Step.t)
      (ls: Armada.State.t)
    : GTot (list Armada.Step.t) =
  
let idx, steps = u tid lsteps ls in
steps