proposition: Corollary to_gregex_weq {L: laws X} n m e f fp: e_level e + e_level f ≪ BKA -> (let v := vars (e_pls e f) in to_gregex v n m e ≡ to_gregex v n m f) -> eval fp n m e ≡ eval fp n m f.
proof: Proof. intros Hl H. rewrite 2(to_gregex_eval (vars (e_pls e f))) by (solve_lower' || simpl (vars _); rewrite union_app; lattice). apply H, L. Qed.
imports: lsyntax ordinal lset positives kat gregex syntax