proposition: Lemma existEdom_proof : forall x i, R x (f (S i)) -> exists y, E x y /\ R y (f (S (S i))).
proof: Proof. intros. destruct (hyp1 (S i)). apply hyp2. exists (g (S i)). split; auto. exists (f (S i)). split; auto. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)