val which_initializers_are_intros:list bool
val which_initializers_are_intros:list bool
let which_initializers_are_intros: list bool =
  [
    false; // The first initializer in B.global_initializers is a, which is not being introduced
    true;  // b *is* being introduced
    false; // c is not being introduced
    true;  // d is being introduced
    false; // e is not being introduced
  ]
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";
  ]

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
  ]
/
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 Prims.bool
Prims.Cons Prims.bool Prims.Nil
let which_initializers_are_intros:list bool =
  
[false; true; false; true; false]