∀ f x1 x2 y1 y2, x1 = x2 ⇒ y1 = y2 ⇒ (f x1 y1) = (f x2 y2)

Theorem eq_f2 : forall A, forall B, forall C, forall (f:(A -> B -> C)), forall (x1:A), forall (x2:A), forall (y1:B), forall (y2:B), (eq (A) x1 x2) -> (eq (B) y1 y2) -> eq (C) (f x1 y1) (f x2 y2).

theorem eq_f2 : \forall A. \forall B. \forall C. \forall (f:A -> B -> C). \forall (x1:A). \forall (x2:A). \forall (y1:B). \forall (y2:B). ((eq) (A) x1 x2) -> ((eq) (B) y1 y2) -> (eq) (C) (f x1 y1) (f x2 y2).

theorem eq_f2 : forall (A : Type) , forall (B : Type) , forall (C : Type) , forall (f:(A) -> (B) -> C) , forall (x1:A) , forall (x2:A) , forall (y1:B) , forall (y2:B) , ((((logic.eq_) (A)) (x1)) (x2)) -> ((((logic.eq_) (B)) (y1)) (y2)) -> (((logic.eq_) (C)) (((f) (x1)) (y1))) (((f) (x2)) (y2)).

eq_f2 [A:TYPE+,B:TYPE+,C:TYPE+] : LEMMA (FORALL(f:[A -> [B -> C]]):(FORALL(x1:A):(FORALL(x2:A):(FORALL(y1:B):(FORALL(y2:B):(logic_sttfa.eq[A](x1)(x2) => (logic_sttfa.eq[B](y1)(y2) => logic_sttfa.eq[C](f(x1)(y1))(f(x2)(y2)))))))))

Printing for OpenTheory is not working at the moment.