proposition: Lemma Ft_sub : forall s t, Ft (sub s t) = sub (Fs s) (Ft t).
proof: Proof. intros s t. pattern t. apply term_ind with (Q := fun n (ts : vector (term S1) n) => Fv (Vmap (sub s) ts) = Vmap (sub (Fs s)) (Fv ts)); clear t; intros. refl. simpl. apply args_eq. unfold Fv in H. rewrite H, Vmap_cast. refl. refl. simpl. rewrite H, H0. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)