split_ifs <;> rfl
case a.h.e'_3
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ (if h1_y = h1_v then V h1_t else V h1_y) = V (if h1_y = h1_v then h1_t else h1_y)
no goals