PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 1 1 1 1 1 1 1 1

1. T: Type
2. P: TProp
3. Q: TProp
4. t:T. P(t) Q(t)
5. x: T
6. P(x)

Q(x)

By: Witness4 x

Generated subgoal:

14. x: T
5. P(x)
6. P(x) Q(x)
7. (P(x)) (Q(x))
Q(x)


About:
applyuniversefunctionpropall