\ / GNU General Public License Version 2
V_______________________________________________________________ *)
+include "basics/core_notation/pair_2.ma".
include "basics/logic.ma".
(* void *)
(* sigma *)
record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
- pi1:> A
+ pi1: A (* not a coercion due to problems with Cerco *)
; pi2: f pi1
}.