Theorem: FOL.NV.T_21_8
Proof state before:
P_r P_s : Formula
r s : VarName
h1 : IsReplOfVarInFormula r s P_r P_s
h2 : ¬isBoundIn r P_r
h3 : ¬isBoundIn s P_r
⊢ IsProof ((eq_ r s).imp_ (P_r.iff_ P_s))
Tactic:
induction h1
Proof state after:
case pred_const_
P_r P_s : Formula
r s : VarName
name✝ : PredName
n✝ : ℕ
args_u✝ args_v✝ : Fin n✝ → VarName
a✝ : ∀ (i : Fin n✝), args_u✝ i = args_v✝ i ∨ args_u✝ i = r ∧ args_v✝ i = s
h2 : ¬isBoundIn r (pred_const_ name✝ (List.ofFn args_u✝))
h3 : ¬isBoundIn s (pred_const_ name✝ (List.ofFn args_u✝))
⊢ IsProof ((eq_ r s).imp_ ((pred_const_ name✝ (List.ofFn args_u✝)).iff_ (pred_const_ name✝ (List.ofFn args_v✝))))

case pred_var_
P_r P_s : Formula
r s : VarName
name✝ : PredName
n✝ : ℕ
args_u✝ args_v✝ : Fin n✝ → VarName
a✝ : ∀ (i : Fin n✝), args_u✝ i = args_v✝ i ∨ args_u✝ i = r ∧ args_v✝ i = s
h2 : ¬isBoundIn r (pred_var_ name✝ (List.ofFn args_u✝))
h3 : ¬isBoundIn s (pred_var_ name✝ (List.ofFn args_u✝))
⊢ IsProof ((eq_ r s).imp_ ((pred_var_ name✝ (List.ofFn args_u✝)).iff_ (pred_var_ name✝ (List.ofFn args_v✝))))

case eq_
P_r P_s : Formula
r s x_u✝ y_u✝ x_v✝ y_v✝ : VarName
a✝¹ : x_u✝ = x_v✝ ∨ x_u✝ = r ∧ x_v✝ = s
a✝ : y_u✝ = y_v✝ ∨ y_u✝ = r ∧ y_v✝ = s
h2 : ¬isBoundIn r (eq_ x_u✝ y_u✝)
h3 : ¬isBoundIn s (eq_ x_u✝ y_u✝)
⊢ IsProof ((eq_ r s).imp_ ((eq_ x_u✝ y_u✝).iff_ (eq_ x_v✝ y_v✝)))

case true_
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ (true_.iff_ true_))

case false_
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r false_
h3 : ¬isBoundIn s false_
⊢ IsProof ((eq_ r s).imp_ (false_.iff_ false_))

case not_
P_r P_s : Formula
r s : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfVarInFormula r s P_u✝ P_v✝
a_ih✝ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
h2 : ¬isBoundIn r P_u✝.not_
h3 : ¬isBoundIn s P_u✝.not_
⊢ IsProof ((eq_ r s).imp_ (P_u✝.not_.iff_ P_v✝.not_))

case imp_
P_r P_s : Formula
r s : VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfVarInFormula r s P_u✝ P_v✝
a✝ : IsReplOfVarInFormula r s Q_u✝ Q_v✝
a_ih✝¹ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ : ¬isBoundIn r Q_u✝ → ¬isBoundIn s Q_u✝ → IsProof ((eq_ r s).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ¬isBoundIn r (P_u✝.imp_ Q_u✝)
h3 : ¬isBoundIn s (P_u✝.imp_ Q_u✝)
⊢ IsProof ((eq_ r s).imp_ ((P_u✝.imp_ Q_u✝).iff_ (P_v✝.imp_ Q_v✝)))

case and_
P_r P_s : Formula
r s : VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfVarInFormula r s P_u✝ P_v✝
a✝ : IsReplOfVarInFormula r s Q_u✝ Q_v✝
a_ih✝¹ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ : ¬isBoundIn r Q_u✝ → ¬isBoundIn s Q_u✝ → IsProof ((eq_ r s).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ¬isBoundIn r (P_u✝.and_ Q_u✝)
h3 : ¬isBoundIn s (P_u✝.and_ Q_u✝)
⊢ IsProof ((eq_ r s).imp_ ((P_u✝.and_ Q_u✝).iff_ (P_v✝.and_ Q_v✝)))

case or_
P_r P_s : Formula
r s : VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfVarInFormula r s P_u✝ P_v✝
a✝ : IsReplOfVarInFormula r s Q_u✝ Q_v✝
a_ih✝¹ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ : ¬isBoundIn r Q_u✝ → ¬isBoundIn s Q_u✝ → IsProof ((eq_ r s).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ¬isBoundIn r (P_u✝.or_ Q_u✝)
h3 : ¬isBoundIn s (P_u✝.or_ Q_u✝)
⊢ IsProof ((eq_ r s).imp_ ((P_u✝.or_ Q_u✝).iff_ (P_v✝.or_ Q_v✝)))

case iff_
P_r P_s : Formula
r s : VarName
P_u✝ Q_u✝ P_v✝ Q_v✝ : Formula
a✝¹ : IsReplOfVarInFormula r s P_u✝ P_v✝
a✝ : IsReplOfVarInFormula r s Q_u✝ Q_v✝
a_ih✝¹ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
a_ih✝ : ¬isBoundIn r Q_u✝ → ¬isBoundIn s Q_u✝ → IsProof ((eq_ r s).imp_ (Q_u✝.iff_ Q_v✝))
h2 : ¬isBoundIn r (P_u✝.iff_ Q_u✝)
h3 : ¬isBoundIn s (P_u✝.iff_ Q_u✝)
⊢ IsProof ((eq_ r s).imp_ ((P_u✝.iff_ Q_u✝).iff_ (P_v✝.iff_ Q_v✝)))

case forall_
P_r P_s : Formula
r s x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfVarInFormula r s P_u✝ P_v✝
a_ih✝ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
h2 : ¬isBoundIn r (forall_ x✝ P_u✝)
h3 : ¬isBoundIn s (forall_ x✝ P_u✝)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x✝ P_u✝).iff_ (forall_ x✝ P_v✝)))

case exists_
P_r P_s : Formula
r s x✝ : VarName
P_u✝ P_v✝ : Formula
a✝ : IsReplOfVarInFormula r s P_u✝ P_v✝
a_ih✝ : ¬isBoundIn r P_u✝ → ¬isBoundIn s P_u✝ → IsProof ((eq_ r s).imp_ (P_u✝.iff_ P_v✝))
h2 : ¬isBoundIn r (exists_ x✝ P_u✝)
h3 : ¬isBoundIn s (exists_ x✝ P_u✝)
⊢ IsProof ((eq_ r s).imp_ ((exists_ x✝ P_u✝).iff_ (exists_ x✝ P_v✝)))