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