apply IsAxiom.eq_2_pred_const_
case a
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsAxiom
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
no goals