proposition: Lemma rel_mem_spec p rel: reflect (In p rel) (rel_mem p rel).
proof: Proof. induction rel. constructor. tauto. simpl rel_mem. case eqb_spec. intros <-. constructor. now left. case IHrel; constructor. now right. intros [?|?]; congruence. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex