#396 New reasoners on inductive types

[Guillaume Verdier]

Currently, reasoners support on inductive types is basically limited to induction and distinct case.
Several other ones would be very useful, such as:
- injectivity of constructors (e.g., C(x)=C(y) implies x=y)
- constructors form a partition of the datatype (and therefore Nil∈List(T) and Nil≠Cons(h, t) for example, for the usual List datatype)
- set membership of constructors arguments (e.g., Cons(h, t)∈List(ℕ) implies h∈ℕ and t∈List(ℕ), which is currently provable through some clever use of ah and distinct case, but is cumbersome)

[Laurent Voisin]

The last case could also be part of the generalized modus ponens reasoner, as it is quite necessary to perform inductive proofs.

[Guillaume Verdier]

The suggested rules have either been directly implemented or are now easily provable. The changes have been merged in commit [160fb8].