proposition: Lemma incl_Frs : forall R S, R [<=] S -> Frs R [<=] Frs S.
proof: Proof. intros. intros a' H0. do 2 destruct H0. subst. exists x. fo. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)