[Feature request] More generated subterm lemmas for a datatype

[clementblaudeau]

When working with datatypes, and writing theorems involving subterms, I often have to carefully expand subterm at precise positions in my proofs, which make them less automated and more fragile. I believe the following things could be really useful for users working with subterms of datatypes:

1. Having a subterm transitivity lemma for free (in the generated declarations) that goes as follows : subterm_transitivity: LEMMA ∀ e1, e2, e3 : subterm(e1, e2) ∧ subterm(e2, e3) ⇒ subterm(e1, e3). The proof is doable by induction but cumbersome.
2. Having a set of rewrite lemmas for subterm (that could be used as auto-rewrites) for each of the constructors, to facilitate the proof work. Adding subterm as a rewrite unfolds too much, as the case analysis is not at top level.

Concretely, this would mean that for a given datatype:

my_datatype: DATATYPE
  BEGIN
     base_case(t:T): base_case
     unary_case(u1: my_datatype): unary_case?
     binary_case(u1, u2: my_datatype): binary_case?
END my_datatype

One would get for free the following (in addition to all the automatically generated)

subterm_transitivity: LEMMA ∀ (e1, e2, e3 : my_datatype): subterm(e1, e2) ∧ subterm(e2, e3) ⇒ subterm(e1, e3)
subterm_base_case: LEMMA ∀(t:T) (e: my_datatype): subterm(e, base_case(t)) = (e = base_case(t))
subterm_unary_case: LEMMA ∀(t:T) (e, u1: my_datatype): subterm(e, unary_case(u1)) = (e = unary_case(u1) OR subterm(e, u1))
subterm_binary_case: LEMMA ∀(t:T) (e, u1, u2: my_datatype): subterm(e, binary_case(u1,u2)) = (e = binary_case(u1,u2) OR subterm(e, u1) OR subterm(e, u2))

And the user could add the rewrites to his theory, saving himself a lot of expands

AUTO_REWRITE+ subterm_base_case, subterm_unary_case, subterm_binary_case

(This might be doable by changing the definition of subterm and adding it as rewrite, but it would not be retro-compatible I guess.)

I believe that could be a great addition to the (already very rich) datatype feature!