proposition: Lemma rule_eq : forall a b : rule, (lhs a = lhs b /\ rhs a = rhs b) <-> a = b.
proof: Proof. intros. destruct a. destruct b. split; intros. destruct H. simpl in *. subst. refl. rewrite H. simpl. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)