proposition: Lemma ISComp_split : IS (E @ R) f -> exists g, ISMod E R f g.
proof: Proof. intros. assert (Hi : forall i, exists x, E (f i) x /\ R x (f (S i))). intro. destruct (H i). exists x. intuition. 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)