proposition: Lemma G_clean n m (e: guards n m): clean e -> gl (G (teval e)) ≡ R (v (o (teval e))).
proof: Proof. intro He. rewrite o_sup, v_sup, lang_sup, R.lang_sup, gl_sup. apply sup_weq'. reflexivity. intros g Hg. apply He, Hg. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms