congr! 1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ ¬Holds D I V E phi ↔ ¬Holds D I V' E phi'
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi ↔ Holds D I V' E phi'