apply IsDeduct.mp_ ((forall_ u P_u).imp_ (forall_ v P_v))
case a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v)))
case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅
    (((forall_ u P_u).imp_ (forall_ v P_v)).imp_
      (((forall_ v P_v).imp_ (forall_ u P_u)).imp_ ((forall_ u P_u).iff_ (forall_ v P_v))))

case a.a
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right_left : ¬isFreeIn u P_v
h1_right_right_left : fastAdmits u v P_u
h1_right_right_right_left : fastAdmits v u P_v
h1_right_right_right_right_left : P_v = fastReplaceFree u v P_u
h1_right_right_right_right_right : P_u = fastReplaceFree v u P_v
⊢ IsDeduct ∅ ((forall_ u P_u).imp_ (forall_ v P_v))