From b7ed6bcd128fd6ab39729e400d9117f6a96c8148 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 21 Jun 2022 10:31:53 +0200
Subject: [PATCH] Make it a functional equality.
---
Lebesgue/Set_theory/Set_base.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Lebesgue/Set_theory/Set_base.v b/Lebesgue/Set_theory/Set_base.v
index c22db4ca..e4d81173 100644
--- a/Lebesgue/Set_theory/Set_base.v
+++ b/Lebesgue/Set_theory/Set_base.v
@@ -2491,9 +2491,9 @@ Variable f : U1 -> U2.
(** Facts about image. *)
-Lemma image_id : forall {U : Type} (A : set U), image id A = A.
+Lemma image_id : forall {U : Type}, @image U U id = id.
Proof.
-intros; apply set_ext_equiv; split; intros x Hx.
+intros; apply fun_ext; intros A; apply set_ext_equiv; split; intros x Hx.
induction Hx as [x Hx]; easy.
rewrite <- id_eq; easy.
Qed.
--
GitLab