diff options
Diffstat (limited to 'src/Util/Sigma.v')
| -rw-r--r-- | src/Util/Sigma.v | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 693b8ef00..1c30219b7 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -211,25 +211,6 @@ Section ex. Defined. End ex. -(* Lift foralls out of sig proofs *) -Definition lift1_sig {A C} (P:A->C->Prop) - (op_sig : forall (a:A), {c | P a c}) : - { op : A -> C | forall (a:A), P a (op a) } - := exist - (fun op => forall a, P a (op a)) - (fun a => proj1_sig (op_sig a)) - (fun a => proj2_sig (op_sig a)) -. - -(* Lift foralls out of sig proofs *) -Definition lift2_sig {A B C} (P:A->B->C->Prop) - (op_sig : forall (a:A) (b:B), {c | P a b c}) : - { op : A -> B -> C | forall (a:A) (b:B), P a b (op a b) } - := exist - (fun op => forall a b, P a b (op a b)) - (fun a b => proj1_sig (op_sig a b)) - (fun a b => proj2_sig (op_sig a b)). - Definition projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q := let 'existT a p := x in existT Q a (f a p). Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q |