simp only [def_iff_]
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)).iff_ (forall_ v (forall_ u 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))).and_
          ((forall_ v (forall_ u P)).imp_ (forall_ u (forall_ v P))))))