add ex Exists

coq · Dec 28, 2024 · 1b6e0df · 1b6e0df
1 parent 47df7aa
commit 1b6e0df
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/src/Tutorial_intro_patterns.v b/src/Tutorial_intro_patterns.v
@@ -223,6 +223,16 @@ Proof.
   intros * (p & q & r & h). 
 Abort.
 
+(** A particularly useful case is to introduce existential quantifications.
+*)
+
+Goal forall P Q (f : forall x y, P x y -> Q x y), 
+     (exists (x y: nat), P x y) -> (exists (x y : nat), Q x y).
+Proof.
+  intros P Q f (x & y & Pxy).
+  exists x, y. apply f. assumption.
+Qed.
+
 
 
 (** ** 3. Rewriting Lemmas *)