1
Require Coq.Arith.Arith.
3
Require Import Coq.subtac.Utils.
4
Program Fixpoint id (n : nat) : { x : nat | x = n } :=
11
pose (subset_simpl (id p)).
22
Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
25
Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
26
if le_gt_dec n 0 then 0
27
else S (id_if (pred n)).
31
pose (subset_simpl (id_if (pred n))).
34
induction n ; auto with arith.
38
Extraction id_if_instance.
40
Notation "( x & y )" := (@existS _ _ x y) : core_scope.
42
Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=