Document refinement rules (#656)
Document refinement rules (#656)

* Document refinement rules for nat, void

* Document some refinement rules for S1

* Document refinement rules for int

* Document some refinement rules for path

* Fix documentation of path refinement rules

* Document missing refinement rules for path

* Fix documentation of path/eqtype rule

* Document refinement rules for line

* Fix documentation of s1/eq/s1-rec rule

* Document some refinement rules for pushout

* Fix documentation of path refinement rules

* Fix documentation of s1/beta/loop and pushout/beta/glue

* Document refinement rules for =

* Document refinement rules for V

* Document refinement rules for U

* Document refinement rules for coe

* Document refinement rules for coeq (except fcom)

* Document 'hcom/eq' rule

* More line breaks in refinement rule documentation

RedPRL/sml-redprl,JonPRL/sml-red-jonprl