The {a^(2n)b^n} language

This file defines {a^(2n)b^n | n in N} over Bool, with false = a and true = b, and proves it is context-free.

theorem quotientLeftBlockCore_eq_hom : quotientLeftBlockCore = anbn.homomorphicImage fun (b : Bool) => if b = true then [true] else [false, false]

theorem CF_quotientLeftBlockCore : is_CF quotientLeftBlockCore