proposition: Lemma arrow_extensionality : forall (x y : Type) (u v : x -> y), (forall a : x, u a = v a) -> u = v.
proof: Proof. intros x y. change (forall u v : forall a : x, (fun i : x => y) a, (forall a : x, u a = v a) -> u = v) in |- *. intros. apply prod_extensionality. assumption. Qed.
imports: Arith