Make pure aliases abbreviations.

Mv fun_ext2 stuff to Function.

Logic/logic_compl.v

@@ -62,53 +62,32 @@ From Coq Require Export ClassicalDescription ClassicalChoice.
 From Coq Require Export IndefiniteDescription.
 
 
+Notation fun_ext_rev := (equal_f).
+Notation prop_ext := (propositional_extensionality).
+Notation proof_irrel := (proof_irrelevance).
+Notation classic_dec := (excluded_middle_informative).
+Notation ex_EX := (constructive_indefinite_description).
+
+
 Section Aliases.
 
+(* Make functions implicit! *)
 Lemma fun_ext :
   forall {T1 T2 : Type} {f g : T1 -> T2}, (forall x1, f x1 = g x1) -> f = g.
 Proof. intros T1 T2; exact functional_extensionality. Qed.
 
-Lemma fun_ext_rev :
-  forall {T1 T2 : Type} {f g : T1 -> T2}, f = g -> forall x1, f x1 = g x1.
-Proof. intros T1 T2 f g; exact equal_f. Qed.
-
-Lemma fun_ext2 :
-  forall {T1 T2 T3 : Type} {f g : T1 -> T2 -> T3},
-    (forall x1 x2, f x1 x2 = g x1 x2) -> f = g.
-Proof. intros; do 2 (apply fun_ext; intro); easy. Qed.
-
-Lemma fun_ext2_rev :
-  forall {T1 T2 T3 : Type} {f g : T1 -> T2 -> T3},
-    f = g -> forall x1 x2, f x1 x2 = g x1 x2.
-Proof. intros; do 2 apply fun_ext_rev; easy. Qed.
-
-Lemma prop_ext : forall (P Q : Prop), P <-> Q -> P = Q.
-Proof. exact propositional_extensionality. Qed.
-
-Lemma proof_irrel : forall (H : Prop) (P Q : H), P = Q.
-Proof. exact proof_irrelevance. Qed.
-
-Lemma classic_dec : forall (P : Prop), {P} + {~ P}.
-Proof. exact excluded_middle_informative. Qed.
-
 (* Make types implicit! *)
 Lemma unique_choice :
   forall {A B : Type} (R : A -> B -> Prop),
     (forall x, exists! y, R x y) -> exists f, forall x, R x (f x).
 Proof. exact unique_choice. Qed.
 
-Lemma ex_EX :
-  forall {T : Type} (P : T -> Prop), (exists x, P x) -> {x | P x}.
-Proof. exact constructive_indefinite_description. Qed.
-
 End Aliases.
 
 
 Tactic Notation "fun_ext" := apply fun_ext; intro.
 Tactic Notation "fun_ext" ident(x) := apply fun_ext; intros x.
 Tactic Notation "fun_ext" ident(x) ident(y) := fun_ext x; fun_ext y.
-Tactic Notation "fun_ext2" := apply fun_ext2; intro; intro.
-Tactic Notation "fun_ext2" ident(x) ident(y) := fun_ext x y.
 
 
 Section Logic_Def.

Subsets/Function.v

@@ -161,6 +161,16 @@ Lemma fun_ext_contra_equiv :
   forall {f g : U1 -> U2},  f <> g <-> exists x1, f x1 <> g x1.
 Proof. intros; split; [apply fun_ext_contra | apply fun_ext_contra_rev]. Qed.
 
+Lemma fun_ext2 :
+  forall {T1 T2 T3 : Type} {f g : T1 -> T2 -> T3},
+    (forall x1 x2, f x1 x2 = g x1 x2) -> f = g.
+Proof. intros; do 2 (apply fun_ext; intro); easy. Qed.
+
+Lemma fun_ext2_rev :
+  forall {T1 T2 T3 : Type} {f g : T1 -> T2 -> T3},
+    f = g -> forall x1 x2, f x1 x2 = g x1 x2.
+Proof. intros; do 2 apply fun_ext_rev; easy. Qed.
+
 End Prop_Facts0.
 
 
@@ -172,6 +182,9 @@ Ltac fun_unfold :=
 Ltac fun_auto := fun_unfold; subset_auto.
 
 Tactic Notation "fun_ext_auto" ident(x) := fun_ext x; fun_auto.
+
+Tactic Notation "fun_ext2" := apply fun_ext2; intro; intro.
+Tactic Notation "fun_ext2" ident(x) ident(y) := fun_ext x y.
 Tactic Notation "fun_ext2_auto" ident(x) ident(y) := fun_ext2 x y; fun_auto.