proposition: Lemma Ft_fill : forall t c, Ft (fill c t) = fill (Fc c) (Ft t).
proof: Proof. induction c; intros. refl. simpl. apply args_eq. rewrite Vmap_cast, Vmap_app. simpl. rewrite Vcast_cast, IHc. apply Vcast_pi. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)