proposition: Lemma Fv_epi : forall n (ts : vector (term S2) n), Fv HF (Fv HG ts) = ts.
proof: Proof. induction ts; simpl; intros. refl. rewrite IHts, Ft_epi. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)