(* Version: 17.09. *)

# Axiomatic Assumptions

For our development, we have to extend Coq with two well known axiomatic assumptions, namely*functional extensionality*and

*propositional extensionality*. The latter entails

*proof irrelevance*.

## Functional Extensionality

We import the axiom from the Coq Standard Library and derive a utility tactic to make the assumption practically usable.
Require Import Coq.Logic.FunctionalExtensionality.

Require Import Program.Tactics.

Tactic Notation "nointr" tactic(t) :=

let m := fresh "marker" in

pose (m := tt);

t; revert_until m; clear m.

Ltac fext := nointr repeat (

match goal with

[ |- ?x = ?y ] =>

(refine (@functional_extensionality_dep _ _ _ _ _) ||

refine (@forall_extensionality _ _ _ _) ||

refine (@forall_extensionalityP _ _ _ _) ||

refine (@forall_extensionalityS _ _ _ _)); intro

end).

Require Import Program.Tactics.

Tactic Notation "nointr" tactic(t) :=

let m := fresh "marker" in

pose (m := tt);

t; revert_until m; clear m.

Ltac fext := nointr repeat (

match goal with

[ |- ?x = ?y ] =>

(refine (@functional_extensionality_dep _ _ _ _ _) ||

refine (@forall_extensionality _ _ _ _) ||

refine (@forall_extensionalityP _ _ _ _) ||

refine (@forall_extensionalityS _ _ _ _)); intro

end).