exact IsAxiom.eq_2_pred_const_ name n args_u args_v
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))))))
no goals