permut_app_inv (PermutLib.v)
Closed this issue · 1 comments
Ayertienna commented
Judging from how it's done in Sorting/Permutation.v, this is not a simple thing. It will probably need a stronger/different induction principle as well...
Ayertienna commented
Ugly, but done.