proposition: Lemma symbs_fill_intro : forall t c, csymbs c ++ symbs t [= symbs (fill c t).
proof: Proof. induction c. simpl. refl. simpl csymbs. simpl fill. rewrite symbs_fun, symbs_vec_cast, symbs_vec_app, symbs_vec_cons, <- app_comm_cons, app_ass. intro x. simpl. intro H. destruct H. subst. left. refl. right. revert x H. apply appl_incl. apply app_com_incl. apply appr_incl. exact IHc. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)