proposition: Lemma Set_RunsTo_characterization: forall (vlen vtmp vpos vtup v : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (fset : GLabelMap.key) (initial_state st' : 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 -> RunsTo env (Call vtmp fset [[[vtup;vpos;v]]]) initial_state st' -> M.Equal st' ([vtmp |> QsADTs.SCAZero]::[vtup |> ADT (QsADTs.WTuple (Array.upd tup pos val))]::initial_state).
proof: Proof. repeat QS_t. reflexivity. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core