From 57e22f6009cdd46c788d8e9d81fb7d1492a40ad5 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 27 Feb 2017 15:46:42 -0500 Subject: Added operation (including creating ) --- src/Util/Sigma.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/Sigma.v') diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 2f7719ab8..96a59e705 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -201,6 +201,16 @@ 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}) : -- cgit v1.2.3