proposition: Lemma ISMod_comp : exists g', ISMod E R f g'.
proof: Proof. assert (Hi : forall i, exists x, E (f i) x /\ R x (f (S i))). intro. destruct (hyp1 i). destruct H0. exists x. split; intuition. apply TE with (g i); auto. pose (Hgi := fun i => (constructive_indefinite_description _ (Hi i))). exists (fun i => proj1_sig (Hgi i)). intro. apply (proj2_sig (Hgi i)). Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)