cases a2
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
a2 : V x_0 = V y_0 ∧ V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1
case intro
Δ : List Formula
F : Formula
x_0 x_1 y_0 y_1 : VarName
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
a✝ : ∀ H ∈ [], Holds D I V E H
left✝ : V x_0 = V y_0
right✝ : V x_1 = V y_1
⊢ V x_0 = V x_1 ↔ V y_0 = V y_1