proposition: Corollary kat_weq_dec `{L: laws} f' fs fp n m (e f: @kat_expr X f' fs n m): e_level e + e_level f ≪ BKA -> (let v := vars (e_pls e f) in eqb_kat (gerase (to_gregex v n m e)) (gerase (to_gregex v n m f)) = Some true) -> eval fp n m e ≡ eval fp n m f.
proof: Proof. intros Hl H. apply to_gregex_weq. assumption. apply kat_untype_weq, eqb_kat_correct, H. Qed.
imports: boolean ugregex_dec kat_reification kat_untyping kat_completeness