Inversion Better support for proofs with indexed type families in Coq Requirements Coq 8.5pl1 Available from https://coq.inria.fr/download SSReflect and Mathematical Components 1.6 Available from https://math-comp.github.io/math-comp/