Split off liftn_sig, add lift{3,4}_sig

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