simp only [Similar] at *
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ Similar P_u.not_ P_v.not_ u v
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u.not_ ∧
    ¬isFreeIn u P_v.not_ ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_