cases h1_right
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
h1_right :
  ¬isFreeIn u P_v ∧
    fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))
case intro
P_u P_v : Formula
u v : VarName
h1_left : ¬isFreeIn v P_u
left✝ : ¬isFreeIn u P_v
right✝ : fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))