solve_proper: add support for subrelation

I realized that solve_proper cannot currently prove things like NonExpansive (λ x, ⌜a = x⌝), which is a bit of a bummer. So this adds the infrastructure required to make that work.

added 1 commit

• f4a280bb - solve_proper: add support for subrelation

Compare with previous version

mentioned in merge request iris!968 (merged)

added 1 commit

• dfda0cba - solve_proper: add support for subrelation

Compare with previous version

added 1 commit

• 7a094711 - LeibnizEquiv implicitly assumes Equiv

Compare with previous version

added 88 commits

• 7a094711...f76ff8d7 - 86 commits from branch master
• 659d5a9f - solve_proper: add support for subrelation
• 72d14599 - LeibnizEquiv implicitly assumes Equiv

Compare with previous version

added 2 commits

• 289d48d4 - move flip handling to inside f_equiv
• b6c696d6 - move some tactic tests so they can be run with fewer things compiling

Compare with previous version

added 1 commit

• 45b3d2ab - move some tactic tests so they can be run with fewer things compiling

Compare with previous version

added 2 commits

• a86093db - move flip handling to inside f_equiv
• 7409daaf - move some tactic tests so they can be run with fewer things compiling

Compare with previous version

added 3 commits

• e1c74be9 - comments and clarifications
• 1ba9d6a8 - move flip handling to inside f_equiv
• aaa053a1 - move some tactic tests so they can be run with fewer things compiling

Compare with previous version

added 2 commits

• 4946e87d - move flip handling to inside f_equiv and solve_proper_finish
• 3eae32d1 - move some tactic tests so they can be run with fewer things compiling

Compare with previous version

added 2 commits

• f034609e - move flip handling to inside f_equiv and solve_proper_finish
• 9baf783c - move some tactic tests so they can be run with fewer things compiling

Compare with previous version