val all_actions_has_all_actions
  (action: Armada.Action.t)
  (program_statements: list program_statement_t)
  : Lemma (contains_ubool action.program_statement program_statements <==>
             (contains_ubool action (all_actions program_statements)))
val all_actions_has_all_actions
  (action: Armada.Action.t)
  (program_statements: list program_statement_t)
  : Lemma (contains_ubool action.program_statement program_statements <==>
             (contains_ubool action (all_actions program_statements)))
let rec all_actions_has_all_actions
  (action: Armada.Action.t)
  (program_statements: list program_statement_t)
  : Lemma (contains_ubool action.program_statement program_statements <==>
             (contains_ubool action (all_actions program_statements))) =
  match program_statements with
  | [] -> ()
  | hd :: tl -> if eqb hd action.program_statement then () else all_actions_has_all_actions action tl
module Strategies.Semantics.Armada

open Armada.Action
open Armada.Step
open Armada.Program
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Strategies.Semantics
open Util.Behavior
open Util.List
/
Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.Semantics.Armada.fst
action: Armada.Action.t -> program_statements: Prims.list Armada.Action.program_statement_t
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.List.contains_ubool (Mkt?.program_statement action) program_statements <==>
      Spec.List.contains_ubool action (Strategies.Semantics.Armada.all_actions program_statements))
Armada.Action.t Prims.list Armada.Action.program_statement_t Spec.Ubool.eqb Armada.Action.__proj__Mkt__item__program_statement Prims.bool Strategies.Semantics.Armada.all_actions_has_all_actions Prims.unit Prims.l_True Prims.squash Prims.l_iff Spec.List.contains_ubool Strategies.Semantics.Armada.all_actions Prims.Nil FStar.Pervasives.pattern
let rec all_actions_has_all_actions
      (action: Armada.Action.t)
      (program_statements: list program_statement_t)
    : Lemma
    (contains_ubool action.program_statement program_statements <==>
      (contains_ubool action (all_actions program_statements))) =
  
match program_statements with
| [] -> ()
| hd :: tl -> if eqb hd action.program_statement then () else all_actions_has_all_actions action tl