proposition: Lemma Fc_epi : forall c, Fc HF (Fc HG c) = c.
proof: Proof. induction c; simpl; intros. refl. eapply cont_eq_intro with (h1 := eq_refl i) (h2 := eq_refl j). apply FG. hyp. rewrite Fv_epi, Vcast_refl. refl. rewrite Fv_epi, Vcast_refl. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)