proposition: Lemma Frs_app : forall R S a, Frs (union R S) a <-> Frs R a \/ Frs S a.
proof: Proof. intuition. do 3 destruct H; subst. left. exists x. auto. right. exists x. auto. destruct H0. destruct H. subst. exists x. intuition. left. hyp. destruct H0. destruct H. subst. exists x. intuition. right. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)