Library Tools

Ltac caseEq f := generalize (refl_equal f); pattern f at -1; case f.


Index
This page has been generated by coqdoc