proposition: Lemma is_pure_sup I J (f: I -> regex'): (forall i, List.In i J -> is_pure (f i)) -> is_pure (\sup_(i\in J) f i).
proof: Proof. apply P_sup; now constructor. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation