Library Axioms

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.

Index
This page has been generated by coqdoc