From e6e1b2d692c98ad2e0aad00b1aa4322e2af8eabc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 1 Jul 2022 17:26:26 +0200
Subject: [PATCH] Make P an explicit argument.
---
Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
index d7b19fea..40586037 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
@@ -108,8 +108,8 @@ Context {U : Type}. (* Universe. *)
Variable A : set U.
(* TODO: find another name! *)
-Inductive Subset : set_system U -> set_system U :=
- | Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.
+Inductive Subset (P : set_system U) : set_system U :=
+ | Sub : forall B, P B -> incl B A -> Subset P B.
Definition Lift : subset_system A -> set_system U := liftp_any A.
Definition Lift_full : subset_system A -> set_system U :=
--
GitLab