section ‹Terminated Lazy Lists as Quotients of Lazy Lists› text ‹ This file demonstrates the lift_bnf utility for quotients on the example of lazy lists. See the Coinductive AFP entry for a much more extensive library of (terminated) lazy lists. › theory TLList imports Main begin