Proving that lists are not permutations using reflection

Using the notion of permutations defined in this exercise and the counting function defined in this exercise. show that if a list is a permutation of another list, then any natural number occurs as many times in both lists.

Build a specialized reflection tactic ``NoPerm \(n\)'' that solve goals of the form ~perm l l' by finding an element of the first list that does not occur the same number of times in both lists.


This file

Going home