fact: Fixpoint g i := match i with | 0 => proj1_sig (ch_min (H 0)) | S i' => proj1_sig (ch_min (H (S (g i')))) end.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)