Library Tools
Ltac
caseEq f := generalize (
refl_equal
f); pattern f at -1; case f.
Index
This page has been generated by
coqdoc