+
+(*
+ * In theory we'd like to be able to do this (below), but it violates
+ * the Prop/Set separation:
+ *
+ * "Elimination of an inductive object of sort Prop is not allowed on a
+ * predicate in sort Set because proofs can be eliminated only to
+ * build proofs."
+ *)
+(*
+Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
+ match t with
+ | (Terminates_intro t') =>
+ match t' with
+ | (ex_intro x y) => x
+ end
+ end.
+*)
+