proposition: Lemma New_Safe: forall (vlen vtup : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (fnew : GLabelMap.key) (initial_state : State QsADTs.ADTValue) (w: W), StringMap.MapsTo vlen (wrap w) initial_state -> GLabelMap.MapsTo fnew (Axiomatic New) env -> not_mapsto_adt vtup initial_state = true -> ~ Word.wlt w (Word.natToWord 32 2) -> Safe env (Call vtup fnew [[[vlen]]]) initial_state.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call). Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core