proposition: Lemma iter_Iter_ge_commut : forall n p, iter n @ Iter_ge p << Iter_ge p @ iter n.
proof: Proof. unfold inclusion. intros. do 2 destruct H. do 2 destruct H0. assert ((iter x1 @ iter n) x y). eapply incl_elim. apply iter_commut. exists x0. intuition. do 2 destruct H2. exists x2. intuition. exists x1. intuition. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)