I : True.
ninductive False: CProp ≝.
+(* elimination principle *)
+ndefinition False_rect ≝ λP: False → Type.λp: False.
+ match p in False return λp. P p with [].
ndefinition Not: CProp → CProp ≝
λA. A → False.
ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
ex_intro: ∀x:A. P x → Ex A P.
-interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file
+interpretation "exists" 'exists x = (Ex ? x).