apply IsAxiom.eq_2_eq_
case a
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsAxiom
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
no goals