PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 1 1 1 2 3 1 1 1
1. T: Type
2. P: TProp
3. Q: TProp
4. t:T. P(t) Q(t)
5. g: {t:T| Q(t) }{t:T| P(t) }
6. x: T
7. P(x)

x {t:T| Q(t) }
By:
Analyze
THEN
Try Auto
Generated subgoal:

1 Q(x)

About:
membersetapplyuniversefunctionpropall