interpretation "context-free irreducibility (term)"
'NotReducible T = (tif T).
(* Basic inversion lemmas ***************************************************)
interpretation "context-free irreducibility (term)"
'NotReducible T = (tif T).
(* Basic inversion lemmas ***************************************************)