apply T_18_6
case a
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ IsDeduct ∅ ((forall_ u P_u.not_).iff_ (forall_ v P_v.not_))
case a.h1
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