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