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