grind propagation over non-Prop arguments

Stream: lean4

[Robin Carlier]

Consider the very artificial

structure EvenStruct (n : Nat) where
  k : Nat
  hk : 2*k = n

def Even (n : Nat) : Prop := ∃ k, 2*k = n

/-- error: invalid `grind` forward theorem, theorem `even` does not have propositional hypotheses -/
#guard_msgs in
@[grind →]
theorem EvenStruct.even {n : Nat} (S : EvenStruct n) : Even n := ⟨S.k, S.hk⟩

I would like to know ways to make grind learn how to propagate the presence of an EvenStruct n in context to the proposition Even n. Is this possible? Is this what a grind_propagator is made for? If yes, how do I write one?

(My actual use case is of course less simple: I am working with a certain category structure on a type of lists, and the mere existence of a morphism implies the lists are permutations of each others. I would like to have grind propagate to List.Perm from the mere presence of a morphism in context automatically, right now my fix is to add a bunch of have : l.Perm l' := …)

[Jovan Gerbscheid]

This seems like it would be useful in category theory, but I guess this might not have been considered when designing grind?

[Jovan Gerbscheid]

An explicit grind_pattern also doesn't work:

/--
error: invalid pattern, (non-forbidden) application expected
  #0
-/
#guard_msgs in
grind_pattern EvenStruct.even => S