Added operation (including creating )

1 files changed, 10 insertions, 0 deletions

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
@@ -202,6 +202,16 @@ Section ex.
 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) }