fact: Fixpoint ISOfISMod_rec n : { x : A * nat | R (fst x) (f (S (snd x))) } := let P := fun x : A * nat => R (fst x) (f (S (snd x))) in match n with | S n' => let (t, Pt) := ISOfISMod_rec n' in let H := existEdom_proof Pt in let s := constructive_indefinite_description _ H in let (t', Pt') := s in (@exist _ P (t', (S (snd t))) (proj2 Pt')) | 0 => @exist _ P (g 0, 0) (proj2 (hyp1 0)) end.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)