Another example of proof development in LEGO is the proof of the Chinese Remainder Theorem in [McKinna, 1992] which we are currently making consistent with the library so that it can be added to our collection of examples.
Some more examples include a proof of strong normalization for system F [Altenkirch, 1993] and a formalization of Pure Type Systems [McKinna and Pollack, 1993] which may be added to the example collection in the future.