right
case h.e'_2.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi
case h.e'_2.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi