include "logic/connectives.ma".
include "nat/orders.ma".
-alias num (instance 0) = "natural number".
inductive sigma (A:Type) (P:A → Prop) : Type ≝
sigma_intro: ∀a:A. P a → sigma A P.
coercion cic:/matita/test/coercions_propagation/eject.con.
alias num (instance 0) = "natural number".
-
theorem test: ∃n. 0 ≤ n.
apply (S O : ∃n. 0 ≤ n).
autobatch.