proposition: Lemma vars_fill_intro : forall t c, cvars c ++ vars t [= vars (fill c t).
proof: Proof. induction c. simpl. refl. simpl cvars. simpl fill. rewrite vars_fun, vars_vec_cast, vars_vec_app, vars_vec_cons, app_ass. apply appl_incl. apply app_com_incl. apply appr_incl. exact IHc. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)