proposition: Lemma comp_comp : forall C D E, comp (comp C D) E = comp C (comp D E).
proof: Proof. induction C; simpl; intros. refl. rewrite IHC. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)