proposition: Lemma tc_iter : R! << Iter.
proof: Proof. unfold inclusion. induction 1; simpl; intros. exists 0. auto. destruct IHclos_trans1. destruct IHclos_trans2. intuition. exists (x0+x1+1). intuition. eapply incl_elim. apply iter_iter. exists y. auto. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)