<commit_before>-- Tested with the development version of Agda on 25 February 2012.

module Existential where

infixr 7 _,_

postulate
  D   : Set
  P Q : D → Set
  P→Q : ∀ {x} → P x → Q x

data ∃ (P : D → Set) : Set where
  _,_ : (x : D) → P x → ∃ P

∃-elim : {P : D → Set}{Q : Set} → ∃ P → (∀ x → P x → Q) → Q
∃-elim (x , p) h = h x p

thm₁ : ∃ P → ∃ Q
thm₁ h = ∃-elim h (λ x Px → x , P→Q Px)

thm₂ : ∃ P → ∃ Q
thm₂ h = ∃-elim h helper
  where
  helper : ∀ x → P x → ∃ Q
  helper x Px = x , P→Q Px<commit_msg>Updated a note on the existential elimination.<commit_after>-- Tested with the development version of Agda on 26 February 2012.

module Existential where

infixr 7 _,_

postulate
  D   : Set
  P Q : D → Set
  P→Q : ∀ {x} → P x → Q x

data ∃ (P : D → Set) : Set where
  _,_ : (x : D) → P x → ∃ P

∃-elim : {P : D → Set}{Q : Set} → ∃ P → (∀ x → P x → Q) → Q
∃-elim (x , p) h = h x p

-- A proof using the existential elimination.
prf₁ : ∃ P → ∃ Q
prf₁ h = ∃-elim h (λ x Px → x , P→Q Px)

-- A proof using the existential elimination with a helper function.
prf₂ : ∃ P → ∃ Q
prf₂ h = ∃-elim h helper
  where
  helper : ∀ x → P x → ∃ Q
  helper x Px = x , P→Q Px

-- A proof using pattern matching.
prf₃ : ∃ P → ∃ Q
prf₃ (x , Px) = x , P→Q Px
{'fraction_non_alphanumeric': 0.14903846153846154, 'fraction_numerical': 0.011217948717948718, 'mean_word_length': 2.1225, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '476592', 'n_tokens_mistral': 648, 'n_tokens_neox': 579, 'n_words': 278}