proposition: Lemma gl_cup n m (e f: glang n m): gl (e ⊔ f) ≡ gl e ⊔ gl f.
proof: Proof. split. intros [w [-> [H|H]]]; [left|right]; exists w; split; auto. intros [H|H]; destruct H as [w [-> H]]; exists w; split; trivial; (now left) || (now right). Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms