## Stream: Is there code for X?

### Topic: Predicates on predicates involving instances

#### Aaron Anderson (Aug 10 2020 at 07:16):

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 (Aug 10 2020 at 07:17):

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 (Aug 10 2020 at 07:19):

(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 (Aug 10 2020 at 07:43):

I think something like this works:

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


Last updated: May 07 2021 at 22:14 UTC