Predicates on predicates involving instances

Stream: Is there code for X?

[Aaron Anderson]

Is there a smoother way to do this:

def hereditary (P : Π (A : Type u) [group A], Prop) : Prop :=
  ∀ (A : Type u) [i : group A] (B : @subgroup A i), @P A i → P B

[Aaron Anderson]

Where I can define a predicate on predicates on groups, and then have functions like P and subgroup infer that A is a group, without repeatedly using @?

[Aaron Anderson]

(My real intention is to be able to define a Fraisse class based on my definition of first-order substructure, but I think this is a good MWE based only on mathlib https://en.wikipedia.org/wiki/Fra%C3%AFss%C3%A9_limit)

[Eric Wieser]

I think something like this works:

∀ (A : Type u) [i : group A], by exactI ∀ (B : subgroup A), P A → P B