Derive luk-* axioms from nic-*.

This is basically ripped from prop.gh, but with small changes to use defthm to
define -> and -. in terms of -/\
restore accidentally-deleted prop.gh
Polish readme