proposition: Lemma iter_tc : forall n, iter n << R!.
proof: Proof. induction n; intros; simpl. apply incl_tc. refl. unfold inclusion. intros. do 2 destruct H. apply t_trans with x0. apply t_step. exact H. apply IHn. exact H0. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)