Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | extensionality: Handle dependently-used hypotheses | Jason Gross | 2016-09-19 |
| | |||
* | Adding an "extensionality in H" tactic which applies functional | Hugo Herbelin | 2016-09-19 |
extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples. |