Theorem: FOL.NV.T_21_8 (FOL/NV/Margaris/Fol.lean)

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
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✝)))

State before:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ (true_.iff_ true_))
Tactic:
case true_ =>
  simp only [def_iff_]
  simp only [def_and_]
  SC
State after:
no goals

State before:
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 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 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 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✝)))
Tactic:
all_goals
  sorry
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ (true_.iff_ true_))
Tactic:
simp only [def_iff_]
State after:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).and_ (true_.imp_ true_)))

State before:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).and_ (true_.imp_ true_)))
Tactic:
simp only [def_and_]
State after:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).imp_ (true_.imp_ true_).not_).not_)

State before:
P_r P_s : Formula
r s : VarName
h2 : ¬isBoundIn r true_
h3 : ¬isBoundIn s true_
⊢ IsProof ((eq_ r s).imp_ ((true_.imp_ true_).imp_ (true_.imp_ true_).not_).not_)
Tactic:
SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))))
Tactic:
apply
  IsDeduct.mp_
    ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))
State after:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))).imp_
      ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))

case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅ ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))

State before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))).imp_
      ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))
Tactic:
SC
State after:
no goals

State before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅ ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))
Tactic:
apply
  IsDeduct.mp_ ((eq_ r s).imp_ (And_ (List.ofFn fun (i : Fin n) => eq_ (args_u i) (args_v i))))
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
      ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))

case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
      ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))
Tactic:
apply
  IsDeduct.mp_
    ((And_ (List.ofFn fun (i : Fin n) => eq_ (args_u i) (args_v i))).imp_
      ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))
State after:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))

case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
      ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))

State before:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_ ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))
Tactic:
simp only [def_iff_]
State after:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).and_
            ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))))).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).and_
            ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u)))))))

State before:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).and_
            ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))))).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).and_
            ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u)))))))
Tactic:
simp only [def_and_]
State after:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).imp_
              ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))).not_).not_).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).imp_
              ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))).not_).not_)))

State before:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).imp_
              ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))).not_).not_).imp_
      (((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i)))).imp_
        ((eq_ r s).imp_
          (((pred_const_ name (List.ofFn args_u)).imp_ (pred_const_ name (List.ofFn args_v))).imp_
              ((pred_const_ name (List.ofFn args_v)).imp_ (pred_const_ name (List.ofFn args_u))).not_).not_)))
Tactic:
SC
State after:
no goals

State before:
case a.a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
      ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))
Tactic:
apply Forall_spec_id' (List.ofFn args_v)
State after:
case a.a.a.h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (Forall_ (List.ofFn args_v)
      ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
        ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))

State before:
case a.a.a.h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (Forall_ (List.ofFn args_v)
      ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
        ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v)))))
Tactic:
apply Forall_spec_id' (List.ofFn args_u)
State after:
case a.a.a.h1.h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (Forall_ (List.ofFn args_u)
      (Forall_ (List.ofFn args_v)
        ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))

State before:
case a.a.a.h1.h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅
    (Forall_ (List.ofFn args_u)
      (Forall_ (List.ofFn args_v)
        ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a.h1.h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsAxiom
    (Forall_ (List.ofFn args_u)
      (Forall_ (List.ofFn args_v)
        ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))

State before:
case a.a.a.h1.h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsAxiom
    (Forall_ (List.ofFn args_u)
      (Forall_ (List.ofFn args_v)
        ((And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))).imp_
          ((pred_const_ name (List.ofFn args_u)).iff_ (pred_const_ name (List.ofFn args_v))))))
Tactic:
exact IsAxiom.eq_2_pred_const_ name n args_u args_v
State after:
no goals

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (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))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
clear h2
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
h3 : ¬isBoundIn s (pred_const_ name (List.ofFn args_u))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
h3 : ¬isBoundIn s (pred_const_ name (List.ofFn args_u))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
clear h3
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (And_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
simp only [And_]
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
args_u args_v : Fin n → VarName
h1_1 : ∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
induction n
State after:
case a.a.zero
P_r P_s : Formula
r s : VarName
name : PredName
args_u args_v : Fin 0 → VarName
h1_1 : ∀ (i : Fin 0), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

case a.a.succ
P_r P_s : Formula
r s : VarName
name : PredName
n✝ : ℕ
a✝ :
  ∀ (args_u args_v : Fin n✝ → VarName),
    (∀ (i : Fin n✝), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n✝ + 1) → VarName
h1_1 : ∀ (i : Fin (n✝ + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
args_u args_v : Fin 0 → VarName
h1_1 : ∀ (i : Fin 0), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
case _ =>
  simp
  SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
args_u args_v : Fin 0 → VarName
h1_1 : ∀ (i : Fin 0), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
simp
State after:
P_r P_s : Formula
r s : VarName
name : PredName
args_u args_v : Fin 0 → VarName
h1_1 : ∀ (i : Fin 0), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ true_)

State before:
P_r P_s : Formula
r s : VarName
name : PredName
args_u args_v : Fin 0 → VarName
h1_1 : ∀ (i : Fin 0), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ true_)
Tactic:
SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
Tactic:
simp
State after:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    ((eq_ r s).imp_
      ((eq_ (args_u 0) (args_v 0)).and_
        (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    ((eq_ r s).imp_
      ((eq_ (args_u 0) (args_v 0)).and_
        (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))
Tactic:
apply
  IsDeduct.mp_
    ((eq_ r s).imp_
      (List.foldr and_ true_
        (List.ofFn fun (i : Fin n) => eq_ (args_u i.succ) (args_v i.succ))))
State after:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
      ((eq_ r s).imp_
        ((eq_ (args_u 0) (args_v 0)).and_
          (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))))

case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))

State before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
      ((eq_ r s).imp_
        ((eq_ (args_u 0) (args_v 0)).and_
          (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).and_
            (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))))

case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).and_
            (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))))))
Tactic:
simp only [def_and_]
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).imp_
              (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))).not_).not_)))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))).imp_
      (((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ)))).imp_
        ((eq_ r s).imp_
          ((eq_ (args_u 0) (args_v 0)).imp_
              (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))).not_).not_)))
Tactic:
SC
State after:
no goals

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
specialize h1_1 0
State after:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : args_u 0 = args_v 0 ∨ args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
case a.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : args_u 0 = args_v 0 ∨ args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
cases h1_1
State after:
case a.a.inl
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h✝ : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

case a.a.inr
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h✝ : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1 =>
  apply IsDeduct.mp_ (eq_ (args_u 0) (args_v 0))
  case _ =>
    SC
  case _ =>
    simp only [c1]
    apply specId (args_v 0)
    apply IsDeduct.axiom_
    apply IsAxiom.eq_1_
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1 =>
  cases c1
  case _ c1_left c1_right =>
    subst c1_left
    subst c1_right
    SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
apply IsDeduct.mp_ (eq_ (args_u 0) (args_v 0))
State after:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))

case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))
Tactic:
case _ =>
  SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))
Tactic:
case _ =>
  simp only [c1]
  apply specId (args_v 0)
  apply IsDeduct.axiom_
  apply IsAxiom.eq_1_
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0))))
Tactic:
SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_u 0) (args_v 0))
Tactic:
simp only [c1]
State after:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_v 0) (args_v 0))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (eq_ (args_v 0) (args_v 0))
Tactic:
apply specId (args_v 0)
State after:
case h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))

State before:
case h1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsDeduct ∅ (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsAxiom (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))

State before:
case h1.a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = args_v 0
⊢ IsAxiom (forall_ (args_v 0) (eq_ (args_v 0) (args_v 0)))
Tactic:
apply IsAxiom.eq_1_
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1 : args_u 0 = r ∧ args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
cases c1
State after:
case intro
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
left✝ : args_u 0 = r
right✝ : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1_left : args_u 0 = r
c1_right : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
case _ c1_left c1_right =>
  subst c1_left
  subst c1_right
  SC
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
c1_left : args_u 0 = r
c1_right : args_v 0 = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
subst c1_left
State after:
P_r P_s : Formula
s : VarName
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
c1_right : args_v 0 = s
ih :
  ∀ (args_u_1 args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v i ∨ args_u_1 i = args_u 0 ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
P_r P_s : Formula
s : VarName
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
c1_right : args_v 0 = s
ih :
  ∀ (args_u_1 args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v i ∨ args_u_1 i = args_u 0 ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) s).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
subst c1_right
State after:
P_r P_s : Formula
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
ih :
  ∀ (args_u_1 args_v_1 : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v_1 i ∨ args_u_1 i = args_u 0 ∧ args_v_1 i = args_v 0) →
      IsDeduct ∅
        ((eq_ (args_u 0) (args_v 0)).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v_1 i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ (eq_ (args_u 0) (args_v 0)))

State before:
P_r P_s : Formula
name : PredName
n : ℕ
args_u args_v : Fin (n + 1) → VarName
ih :
  ∀ (args_u_1 args_v_1 : Fin n → VarName),
    (∀ (i : Fin n), args_u_1 i = args_v_1 i ∨ args_u_1 i = args_u 0 ∧ args_v_1 i = args_v 0) →
      IsDeduct ∅
        ((eq_ (args_u 0) (args_v 0)).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u_1 i) (args_v_1 i))))
⊢ IsDeduct ∅ ((eq_ (args_u 0) (args_v 0)).imp_ (eq_ (args_u 0) (args_v 0)))
Tactic:
SC
State after:
no goals

State before:
case a
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i.succ) (args_v i.succ))))
Tactic:
apply ih
State after:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ ∀ (i : Fin n), args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s

State before:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
⊢ ∀ (i : Fin n), args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Tactic:
intro i
State after:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
i : Fin n
⊢ args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s

State before:
case a.h1_1
P_r P_s : Formula
r s : VarName
name : PredName
n : ℕ
ih :
  ∀ (args_u args_v : Fin n → VarName),
    (∀ (i : Fin n), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s) →
      IsDeduct ∅ ((eq_ r s).imp_ (List.foldr and_ true_ (List.ofFn fun i => eq_ (args_u i) (args_v i))))
args_u args_v : Fin (n + 1) → VarName
h1_1 : ∀ (i : Fin (n + 1)), args_u i = args_v i ∨ args_u i = r ∧ args_v i = s
i : Fin n
⊢ args_u i.succ = args_v i.succ ∨ args_u i.succ = r ∧ args_v i.succ = s
Tactic:
apply h1_1
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_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_))
Tactic:
simp only [isBoundIn] at h2
State after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u.not_
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))

State before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u.not_
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
simp only [isBoundIn] at h3
State after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))

State before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
specialize h1_ih h2 h3
State after:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))

State before:
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (P_u.iff_ P_v))
State after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_ ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_)))

case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))

State before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_ ((eq_ r s).imp_ (P_u.not_.iff_ P_v.not_)))
Tactic:
simp only [def_iff_]
State after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).and_ (P_v.not_.imp_ P_u.not_))))

State before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).and_ (P_v.not_.imp_ P_u.not_))))
Tactic:
simp only [def_and_]
State after:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).imp_ (P_v.not_.imp_ P_u.not_).not_).not_))

State before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).imp_ (P_v.not_.imp_ P_u.not_).not_).not_))
Tactic:
SC
State after:
no goals

State before:
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih
State after:
no goals

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬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)))
Tactic:
simp only [isBoundIn] at h2
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬(isBoundIn r P_u ∨ isBoundIn r 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)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬(isBoundIn r P_u ∨ isBoundIn r 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)))
Tactic:
push_neg at h2
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2 : ¬isBoundIn r P_u ∧ ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2 : ¬isBoundIn r P_u ∧ ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
cases h2
State after:
case intro
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
left✝ : ¬isBoundIn r P_u
right✝ : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
simp only [isBoundIn] at h3
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬(isBoundIn s P_u ∨ isBoundIn s Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h3 : ¬(isBoundIn s P_u ∨ isBoundIn s Q_u)
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
push_neg at h3
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3 : ¬isBoundIn s P_u ∧ ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3 : ¬isBoundIn s P_u ∧ ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
cases h3
State after:
case intro
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
left✝ : ¬isBoundIn s P_u
right✝ : ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
specialize h1_ih_1 h2_left h3_left
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
specialize h1_ih_2 h2_right h3_right
State after:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))

State before:
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (Q_u.iff_ Q_v))
State after:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v))))

case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (Q_u.iff_ Q_v))

State before:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v))))
Tactic:
apply IsDeduct.mp_ ((eq_ r s).imp_ (P_u.iff_ P_v))
State after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_
      (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))))

case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))

State before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ (P_u.iff_ P_v)).imp_
      (((eq_ r s).imp_ (Q_u.iff_ Q_v)).imp_ ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))))
Tactic:
simp only [def_iff_]
State after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).and_ (Q_v.imp_ Q_u))).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).and_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u))))))

State before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).and_ (P_v.imp_ P_u))).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).and_ (Q_v.imp_ Q_u))).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).and_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u))))))
Tactic:
simp only [def_and_]
State after:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).imp_ (Q_v.imp_ Q_u).not_).not_).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).imp_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u)).not_).not_)))

State before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      (((eq_ r s).imp_ ((Q_u.imp_ Q_v).imp_ (Q_v.imp_ Q_u).not_).not_).imp_
        ((eq_ r s).imp_ (((P_u.imp_ Q_u).imp_ (P_v.imp_ Q_v)).imp_ ((P_v.imp_ Q_v).imp_ (P_u.imp_ Q_u)).not_).not_)))
Tactic:
SC
State after:
no goals

State before:
case a.a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih_1
State after:
no goals

State before:
case a
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h2_left : ¬isBoundIn r P_u
h2_right : ¬isBoundIn r Q_u
h3_left : ¬isBoundIn s P_u
h3_right : ¬isBoundIn s Q_u
h1_ih_1 : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
⊢ IsDeduct ∅ ((eq_ r s).imp_ (Q_u.iff_ Q_v))
Tactic:
exact h1_ih_2
State after:
no goals

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_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)))
Tactic:
simp only [isBoundIn] at h2
State after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬(r = x ∨ isBoundIn r P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬(r = x ∨ isBoundIn r P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
push_neg at h2
State after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2 : r ≠ x ∧ ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2 : r ≠ x ∧ ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
cases h2
State after:
case intro
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
left✝ : r ≠ x
right✝ : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬isBoundIn s (forall_ x P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
simp only [isBoundIn] at h3
State after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬(s = x ∨ isBoundIn s P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h3 : ¬(s = x ∨ isBoundIn s P_u)
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
push_neg at h3
State after:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3 : s ≠ x ∧ ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3 : s ≠ x ∧ ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
cases h3
State after:
case intro
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
left✝ : s ≠ x
right✝ : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply deduction_theorem
State after:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct (∅ ∪ {eq_ r s}) ((forall_ x P_u).iff_ (forall_ x P_v))

State before:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct (∅ ∪ {eq_ r s}) ((forall_ x P_u).iff_ (forall_ x P_v))
Tactic:
simp
State after:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x P_u).iff_ (forall_ x P_v))

State before:
case h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x P_u).iff_ (forall_ x P_v))
Tactic:
apply IsDeduct.mp_ (forall_ x (P_u.iff_ P_v))
State after:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (forall_ x (P_u.iff_ P_v))

State before:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))

State before:
case h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((forall_ x (P_u.iff_ P_v)).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
Tactic:
apply T_18_1
State after:
no goals

State before:
case h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (forall_ x (P_u.iff_ P_v))
Tactic:
apply IsDeduct.mp_ (eq_ r s)
State after:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))

case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (eq_ r s)

State before:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))
Tactic:
apply proof_imp_deduct
State after:
case h1.a.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))

State before:
case h1.a.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsProof ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v)))
Tactic:
apply IsDeduct.mp_ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))
State after:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v))).imp_ ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v))))

case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))

State before:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v))).imp_ ((eq_ r s).imp_ (forall_ x (P_u.iff_ P_v))))
Tactic:
apply T_19_TS_21_left
State after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬isFreeIn x (eq_ r s)

State before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬isFreeIn x (eq_ r s)
Tactic:
simp only [isFreeIn]
State after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬(x = r ∨ x = s)

State before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ¬(x = r ∨ x = s)
Tactic:
push_neg
State after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r ∧ x ≠ s

State before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r ∧ x ≠ s
Tactic:
constructor
State after:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r

case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ s

State before:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ r
Tactic:
simp only [ne_comm]
State after:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ r ≠ x

State before:
case h1.a.a.h1.a.h1.left
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ r ≠ x
Tactic:
exact h2_left
State after:
no goals

State before:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ x ≠ s
Tactic:
simp only [ne_comm]
State after:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ s ≠ x

State before:
case h1.a.a.h1.a.h1.right
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ s ≠ x
Tactic:
exact h3_left
State after:
no goals

State before:
case h1.a.a.h1.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ (forall_ x ((eq_ r s).imp_ (P_u.iff_ P_v)))
Tactic:
apply generalization
State after:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))

case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ∀ H ∈ ∅, ¬isFreeIn x H

State before:
case h1.a.a.h1.a.h1
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
Tactic:
exact h1_ih h2_right h3_right
State after:
no goals

State before:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Tactic:
intro H a1
State after:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H

State before:
case h1.a.a.h1.a.h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Tactic:
simp at a1
State after:
no goals

State before:
case h1.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct {eq_ r s} (eq_ r s)
Tactic:
apply IsDeduct.assume_
State after:
case h1.a.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ eq_ r s ∈ {eq_ r s}

State before:
case h1.a.a.a
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ eq_ r s ∈ {eq_ r s}
Tactic:
simp
State after:
no goals

State before:
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✝)))
Tactic:
sorry
State after:
no goals