DCFs are a subset of CFLs

This file shows that DCFs are a subset of the CFLs.

theorem is_CF_of_is_DCF {T : Type} [Fintype T] {L : Language T} (h : is_DCF L) : is_CF L

theorem DCF_subclass_CF {T : Type} [Fintype T] : DCF ⊆ CF

The class of deterministic context-free languages is contained in the class of context-free languages.