| ---- Op | |
| true | |
| false | |
| false | |
| false | |
| ---- Foo 1 | |
| true | |
| false | |
| ---- Foo 2 | |
| true | |
| false | |
| ---- Op 2 | |
| false | |
| true | |
| false | |
| false | |
| ---- Foo 3 | |
| match2.lean:83:0-85:21: error: the '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided |