Axiom fun_extensionality : forall (A B : Type) (f g : A -> B), (forall x, f x = g x) -> f = g. Axiom Proof_irrelevance : forall (P : Prop) (p q : P), p = q.
Axiom