simp only [def_exists_]
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((exists_ u P_u).iff_ (exists_ v P_v))
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_)