ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
#A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.
ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C.
∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
#A; #B; #C; #f; #x1; #x2; #y1; #y2; #E1; #E2; nrewrite > E1; nrewrite > E2;//.