apply IsDeduct.mp_ ((forall_ u P_u.not_).iff_ (forall_ v P_v.not_))
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_)
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_)).imp_ ((forall_ u P_u.not_).not_.iff_ (forall_ v P_v.not_).not_))

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_))