Variety of proofs, primarily for Lists

to demonstrate the usabilty of equational reasoning in HERMIT