The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 Is there already in Coq something like the following and_dep ?

Pierre



Inductive and_dep (P : Prop)(Q : P -> Prop) :Prop :=
conj_dep : forall (p:P), Q p -> and_dep  P Q.

Set Implicit Arguments.

Require Import Ensembles.

Parameters (OT : Type)
          (ordinal : Ensemble OT)
      (critical : forall alpha : OT, ordinal alpha -> Ensemble OT).


(* I prefer to write (Cr alpha) than (Cr H) where H assumes (ordinal alpha)
*)

Definition Cr (alpha : OT) : Ensemble OT :=
  fun beta =>
      and_dep (ordinal alpha) (fun H => (critical  H beta)).