proposition: Lemma ISOfISMod_rec_spec : forall i, E (fst (proj1_sig (ISOfISMod_rec i))) (fst (proj1_sig (ISOfISMod_rec (S i)))).
proof: Proof. induction i; simpl. destruct (constructive_indefinite_description _ (existEdom_proof (proj2 (hyp1 0)))) as [t Pt]. simpl. destruct Pt. auto. destruct (ISOfISMod_rec i) as [t Pt]. destruct (constructive_indefinite_description _ (existEdom_proof Pt)) as [t' Pt']. simpl. destruct (constructive_indefinite_description _ (existEdom_proof (proj2 Pt'))) as [y Py]. simpl. exact (proj1 Py). Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)