proposition: Theorem f2_equal : forall (A B C: Type) (f: A -> B -> C) (x1 x2: A)(y1 y2: B), (x1 = x2 /\ y1 = y2) -> f x1 y1 = f x2 y2.
proof: Proof. intros A B C f x1 x2 y1 y2 eq. destruct eq as [eq1 eq2]. rewrite eq1. rewrite eq2. reflexivity. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)