simp only [HoldsShift D I V F z h1]
D : Type
I : Interpretation D
V : VarAssignment D
x : String
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ (∀ (d : D), Holds D I (shift D V d) F) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (free_ z) d) (Formula.openList 0 [free_ z] F)
D : Type
I : Interpretation D
V : VarAssignment D
x : String
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ (∀ (d : D), Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (free_ z) d) (Formula.openList 0 [free_ z] F)