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