The {b^n a^n} language

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

theorem quotientRightBlockCore_eq_hom : quotientRightBlockCore = anbn.homomorphicImage fun (b : Bool) => if b = true then [false] else [true]

theorem CF_quotientRightBlockCore : is_CF quotientRightBlockCore