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