proposition: Lemma iter_compose : forall p q, iter p @ iter q << iter (p+q+1).
proof: Proof. intros; induction p. assert (S(q) = q+1); auto with *. simpl; rewrite <- H; simpl; intuition. unfold inclusion; intros. simpl in H; repeat destruct H. simpl; unfold compose. exists x1; split; auto with *. unfold inclusion in IHp; eapply IHp. simpl; unfold compose. exists x0; split; auto with *. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)