Set Implicit Arguments.
Axiom ext_eq_Type : forall (D : Type) (R : D -> Type)
(f g : forall (x : D), R x),
(forall x, f x = g x) -> f = g.
Theorem ext_eq : forall (D R : Set) (f g : D -> R),
(forall x, f x = g x) -> f = g.
Theorem ext_eqT : forall (D R : Type) (f g : D -> R),
(forall x, f x = g x) -> f = g.
Theorem ext_eq_dep : forall (R : Set -> Set) (f g : forall (x : Set), R x),
(forall x, f x = g x) -> f = g.