Relations

There are two files, relations.l, and relclosure.l, which give elementary and infinitary lemmas about the algebra of relations. They pre-date the addition of primitive inductive types to LEGO, so use impredicative encodings to get "System F"-like inductive definitions.

In both files, a glaring omission is the failure to show that all the operations on relations introduced are in fact extensional with respect to EQRel. Much more could fruitfully be added.