fact: Definition ISOfISMod n := match n with | S n' => (fst (proj1_sig (ISOfISMod_rec n'))) | 0 => f 0 end.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)