fact: Definition ProgOk {av} ext env prog (initial_tstate final_tstate: Telescope av) := forall initial_state: State av, (initial_state ≲ initial_tstate ∪ ext) -> Safe env prog initial_state /\ forall final_state: State av, @RunsTo _ env prog initial_state final_state -> (final_state ≲ final_tstate ∪ ext).
imports: Coq.Strings.String Computation.Core ADTRefinement Bedrock.Platform.Facade.DFacade Bedrock.Platform.Cito.StringMap