proposition: Lemma symbs_fill_elim : forall t c, symbs (fill c t) [= csymbs c ++ symbs t.
proof: Proof. induction c. simpl. refl. simpl fill. rewrite symbs_fun. simpl. intro x. simpl; intro H. destruct H. subst. left. refl. right. ded (in_symbs_vec_elim H). do 2 destruct H0. ded (Vin_cast_elim H0). ded (Vin_app H2). destruct H3. repeat apply in_appl. apply (symbs_vec_in H1 H3). simpl in H3. destruct H3. subst x0. ded (IHc _ H1). rewrite app_ass. apply in_appr. apply in_app_com. apply in_appl. exact H3. apply in_appl. repeat apply in_appr. apply (symbs_vec_in H1 H3). Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)