val vs:list var_id_t
val vs:list var_id_t
let vs: list var_id_t = // introduced variables in no particular order
  [
    "b";
    "d";
  ]
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
/
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.Base.var_id_t
Prims.Cons Armada.Base.var_id_t Prims.Nil
let vs:list var_id_t =
  
["b"; "d"]