Skip to content

Adding telescopes and some useful lemmas.

Ghost User requested to merge telescope into master

These will be used to help define and prove lemmas related to the incoming Accessible typeclass.

Merge request reports