1. Inwersja predykatów indukcyjnych Inversion.v

2. Define a kind of dependently typed lists, where a list’s type index gives a lower bound on how many of its elements satisfy a particular predicate. In particular, for an arbitrary set A and a predicate P over it:
(a) Define a type plist : nat → Set. Each plist n should be a list of As, where it is guaranteed that at least n distinct elements satisfy P. There is wide latitude in choosing how to encode this. You should try to avoid using subset types or any other mechanism based on annotating non-dependent types with propositions after-the-fact.
(b) Define a version of list concatenation that works on plists. The type of this new function should express as much information as possible about the output plist.
(c) Define a function plistOut for translating plists to normal lists.
(d) Define a function plistIn for translating lists to plists. The type of plistIn should make it clear that the best bound on P -matching elements is chosen. You may assume that you are given a dependently typed function for deciding instances of P.
(e) Prove that, for any list ls, plistOut (plistIn ls) = ls. This should be the only part of the exercise where you use tactic-based proving.
(f) Define a function grab : ∀ n (ls : plist (S n)), sig P. That is, when given a plist guaranteed to contain at least one element satisfying P, grab produces such an element. The type family sig is the one we met earlier for sigma types (i.e., dependent pairs of programs and proofs), and sig P is extensionally equivalent to {x : A | P x }, though the latter form uses an eta-expansion of P instead of P itself as the predicate.