proposition: Lemma sub_rules_inv : forall x, sub_rules s1 (sub_rules s2 x) = x.
proof: Proof. induction x. refl. simpl. rewrite sub_rule_inv, IHx. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)