apply C_18_4 (forall_ u P_u) (forall_ v P_v) Q Q' Δ h2
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q'
case h2
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsProof ((forall_ u P_u).iff_ (forall_ v P_v))

case h3
P_u P_v Q Q' : Formula
u v : VarName
Δ : Set Formula
h1 : IsDeduct Δ Q
h2 : IsReplOfFormulaInFormula (forall_ u P_u) (forall_ v P_v) Q Q'
h3 : Similar P_u P_v u v
⊢ IsDeduct Δ Q