val is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  : Lemma
    (requires is_inductive_armada_invariant_of_program inv program)
    (ensures  is_invariant_of_spec inv (program_to_spec program))
val is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  : Lemma
    (requires is_inductive_armada_invariant_of_program inv program)
    (ensures  is_invariant_of_spec inv (program_to_spec program))
let is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  (* see .fsti file for spec *) =
  is_inductive_invariant_of_spec_implies_is_invariant_of_spec inv (program_to_spec program)
module Strategies.Invariant.Armada

open FStar.List.Tot
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Semantics.Armada
open Util.List
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.fst
inv: Strategies.Invariant.invariant_t Armada.State.t -> program: Armada.Program.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.Invariant.Armada.is_inductive_armada_invariant_of_program inv program)
      (ensures
        Strategies.Invariant.is_invariant_of_spec inv (Armada.Program.program_to_spec program))
Strategies.Invariant.invariant_t Armada.State.t Armada.Program.t Strategies.Invariant.is_inductive_invariant_of_spec_implies_is_invariant_of_spec Armada.Program.program_to_spec Prims.unit
let is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
      (inv: invariant_t Armada.State.t)
      (program: Armada.Program.t)
     =
  
is_inductive_invariant_of_spec_implies_is_invariant_of_spec inv (program_to_spec program)