interpretation "exists" 'exists x = (ex ? x).
inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
- ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
+ ex2_intro: ∀ x:A. P x → Q x → ex2 A P Q.
+
+interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2).
+
+lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
+#A0 #P0 #P1 * /2 width=3/
+qed.
(* iff *)
definition iff :=
(* Example to avoid indexing and the consequential creation of ill typed
terms during paramodulation *)
-example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
#A #x #h @(refl ? h: eqProp ? ? ?).
-qed.
+qed-.
theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
#T #t #P #H #p >(lemmaK T t p) @H
-qed.
+qed-.