diff options
Diffstat (limited to 'contrib/subtac/Utils.v')
| -rw-r--r-- | contrib/subtac/Utils.v | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 9acb10ae..db10cb2a 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -1,20 +1,17 @@ Set Implicit Arguments. +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). + +Notation "( x & y )" := (@existS _ _ x y) : core_scope. + Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. intros. induction t. exact x. Defined. -Check proj1_sig. -Lemma subset_simpl : forall (A : Set) (P : A -> Prop) - (t : sig P), P (proj1_sig t). -Proof. -intros. -induction t. - simpl ; auto. -Qed. - Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P), P (ex_pi1 t). intros A P. @@ -23,12 +20,17 @@ simpl. exact p. Defined. + +Notation "` t" := (proj1_sig t) (at level 100) : core_scope. Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, Q) (at level 200, x ident, right associativity). -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). +Lemma subset_simpl : forall (A : Set) (P : A -> Prop) + (t : sig P), P (` t). +Proof. +intros. +induction t. + simpl ; auto. +Qed. -Notation "( x & y )" := (@existS _ _ x y) : core_scope. |