proposition: Lemma comp_eq : forall c d e, comp c d = comp c e <-> d = e.
proof: Proof. split. induction c; simpl; intros. hyp. inversion H. auto. intro. subst. refl. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)