Commit 2023-12-04 23:32 c3269f99

View on Github →

refactor: code cleanup in gcongr (#8796)

  • Extract the default side-goal and main-goal gcongr dischargers into functions
  • Change the default main-goal discharger to gcongr_forward (instead of assumption which is never used)
  • add subset_of_ssubset as a gcongr_forward lemma

Estimated changes