PrintForm Definitions finite sets Sections AutomataTheory Doc

At: not dec is dec 1 1 2 1 1
1. A: Type
2. P: AProp
3. x:A. P(x) P(x)
4. (x:A. P(x))
5. x: A

P(x)
By: InstHyp [x] 3
Generated subgoal:

16. P(x) P(x)
P(x)

About:
applyuniversefunctionpropallorexists