proposition: Lemma beq_rule_ok : forall a b, beq_rule a b = true <-> a = b.
proof: Proof. destruct a as [a1 a2]. destruct b as [b1 b2]. unfold beq_rule. simpl. rewrite andb_eq, !beq_term_ok. split_all. subst. refl. inversion H. auto. inversion H. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)