internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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_]
Proof 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_)))
Theorem: FOL.NV.T_21_8
Proof 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_]
Proof 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_)
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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))))
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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))))
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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))))
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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_]
Proof 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)))))))
Theorem: FOL.NV.T_21_8
Proof 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_]
Proof 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_)))
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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)
Proof 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)))))
Theorem: FOL.NV.T_21_8
Proof 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)
Proof 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))))))
Theorem: FOL.NV.T_21_8
Proof 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_
Proof 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))))))
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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_]
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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
Proof 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))))
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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
Proof 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_)
Theorem: FOL.NV.T_21_8
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.T_21_8
Proof 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
Proof 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)))))