simp only [def_and_]
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))
case a.a
P : Formula
u v : VarName
⊢ IsDeduct ∅
    (((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).imp_
      (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
        (((forall_ u (forall_ v P)).imp_ (forall_ v (forall_ u P))).imp_
            ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))).not_).not_))