apply IsProofAlt.eq_2_pred_const_
F h1_phi : Formula
h1_1_name : PredName
h1_1_n : ℕ
h1_1_xs h1_1_ys : Fin h1_1_n → VarName
⊢ IsProofAlt
    (Forall_ (List.ofFn h1_1_xs)
      (Forall_ (List.ofFn h1_1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_1_xs i) (h1_1_ys i))).imp_
          ((pred_const_ h1_1_name (List.ofFn h1_1_xs)).iff_ (pred_const_ h1_1_name (List.ofFn h1_1_ys))))))
no goals