Skip to content

Allow `InstantiateForall` to weaken sequents

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/inst-weakening into main

This is particularly to fix issues when using instantiation in the presence of assumptions. This is partial progress (and one of the major issues in) #161.

Merge request reports