Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopes

Reviewed-by: mattam82

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 09a32e9483..4d84d61f9f 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -274,6 +274,22 @@ Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
 Register ex as core.ex.type.
+Register ex_intro as core.ex.intro.
+
+Section Projections.
+
+  Variables (A:Prop) (P:A->Prop).
+
+  Definition ex_proj1 (x:ex P) : A :=
+    match x with ex_intro _ a _ => a end.
+
+  Definition ex_proj2 (x:ex P) : P (ex_proj1 x) :=
+    match x with ex_intro _ _ b => b end.
+
+  Register ex_proj1 as core.ex.proj1.
+  Register ex_proj2 as core.ex.proj2.
+
+End Projections.
 
 Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
   ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.