Is there a tactic to expand a forall

Stream: Is there code for X?

[Ben]

If I have h1: ∀ (i : G) f i is there a way to expand that out into two hypothesis / props aka i: G and h1: f i?

[Yaël Dillies]

How does that make sense? Maybe G is empty!

[Ben]

Ah that would be problem I see, what happens if I have non_empty G. I guess I can then use choose to get a G and then get the prop of h1 using h1 my_g