proposition: Lemma ISOfISMod_spec : IS E ISOfISMod.
proof: Proof. intro. case i. simpl. exact (proj1 (hyp1 O)). intros. unfold ISOfISMod. exact (ISOfISMod_rec_spec n). Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)