if eq safe

import Definitions.Def_ResourceScheduling_Graph_ReductionProgram
import Definitions.Def_ResourceScheduling_Graph_RAMSafe
open ResourceScheduling.Graph GraphReg GraphProgram

namespace ResourceScheduling.Graph
theorem if_eq_safe (a b : GraphReg) (p q : Code) (B : ℕ) (P : RAMState GraphReg → Prop)
    (hd : ∀ s x, P s → P (s.set delta x)) (ha : ∀ s x, P s → P (s.set aux x))
    (hp : ∀ s, RAMBound B s → P s → RAMSafe p B s)
    (hq : ∀ s, RAMBound B s → P s → RAMSafe q B s)
    (s : RAMState GraphReg) (hs : RAMBound B s) (hP : P s) : RAMSafe (ifEq a b p q) B s := by sorry
end ResourceScheduling.Graph