proposition: Lemma Ft_epi : forall t, Ft HF (Ft HG t) = t.
proof: Proof. intro t. pattern t; apply term_ind with (Q := fun n (ts : vector (term S2) n) => Vmap (Ft HF) (Vmap (Ft HG) ts) = ts); clear t. refl. intros. simpl. eapply fun_eq_intro with (h:=FG f). rewrite Vmap_cast, !Vcast_cast, H. sym. apply Vcast_refl. refl. intros. simpl. rewrite H, H0. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)