apply
  IsDeduct.mp_ ((eq_ r s).imp_ (And_ (List.ofFn fun (i : Fin n) => eq_ (args_u i) (args_v i))))
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))))
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))))