Potential plugin projects in Template Coq

• Induction principles
• Induction principles for mutual inductive types
• Induction principles for simple nested inductive types only mentioning prod, option and list
• Induction principles for nested inductive types
• Equality deciders (similar to Scheme Equality)
• Finiteness proofs
• Countability (/enumerability) proofs
• Selectors (e.g. is_nil : forall A, list A -> bool and is_cons, or more advanced versions like inv_cons : forall A, list A -> option (A * list A))
• Lenses, extending https://github.com/gmalecha/coq-lens, for instance with proofs
• Subterm relations (similar to Derive Subterm in Equations)
• Show instances, i.e. Show A := show : A -> string
• Sized instances, i.e. Sized A := size : A -> nat/ord