val tds:list object_td_t
val tds:list object_td_t
let tds: list object_td_t = // object type descriptors for the introduced variables in the order corresponding to `vs`
  [
    (ObjectTDAbstract int); // "b" is an abstract int
    (ObjectTDAbstract int); // "d" is an abstract int
  ]
module MyVarIntroProof

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars.Types
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.PCIndices
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Efficient
open Util.ImmutableArray

let vs: list var_id_t = // introduced variables in no particular order
  [
    "b";
    "d";
  ]
/
Util.ImmutableArray.fsti.checked Strategies.VarIntro.Efficient.fsti.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCIndices.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyBProg.fst.checked MyAtomicBProg.fst.checked MyAtomicBInvariant.fst.checked MyAtomicAProg.fst.checked MyAProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyVarIntroProof.fst
Prims.list Armada.Type.object_td_t
Prims.Cons Armada.Type.object_td_t Armada.Type.ObjectTDAbstract Prims.int Prims.Nil
let tds:list object_td_t =
  
[(ObjectTDAbstract int); (ObjectTDAbstract int)]