proposition: Lemma Set_Safe: forall (vtmp vpos vtup v : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (fset : GLabelMap.key) (initial_state : State QsADTs.ADTValue) (tup: TuplesF.tupl) (val pos: W), StringMap.MapsTo v (wrap val) initial_state -> StringMap.MapsTo vpos (wrap pos) initial_state -> StringMap.MapsTo vtup (wrap (FacadeWrapper := WrapInstance (H := BedrockWrapper)) tup) initial_state -> GLabelMap.MapsTo fset (Axiomatic WTupleADTSpec.Put) env -> not_mapsto_adt vtmp initial_state = true -> Word.wlt pos (IL.natToW (Datatypes.length tup)) -> Safe env (Call vtmp fset [[[vtup;vpos;v]]]) initial_state.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call). Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core