This document is a literate Idris2 file that the compiler can understand, and if one uses polymode for eMacs can highlight…
In this document, we outline a proof of Merge For Synthesis for a simple representation of Local type. Merging this into Capable is going to be trifficult!