proposition: Lemma root_preserving : forall R a, is_root_preserving a = true -> In a R -> In a (flat_rules R).
proof: Proof. intros. unfold flat_rules. rewrite in_flat_map. exists a. split_all. unfold flat_rule. rewrite H. simpl. auto. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)