E.g.
Inductive term : Set :=
| ...
.
Instance Traverse_term : Traverse term term :=
{traverse := (fix rec f l e := ...)}.
Goal @TraverseFunctorial term _ term _.
Proof.
constructor. prove_traverse_functorial.
Shown to break:
prove_traverse_functorial
prove_traverse_relative
prove_traverse_var_is_identity
Shown to work:
prove_traverse_var_injective
prove_traverse_identifies_var
E.g.
Shown to break:
prove_traverse_functorialprove_traverse_relativeprove_traverse_var_is_identityShown to work:
prove_traverse_var_injectiveprove_traverse_identifies_var