PrintForm Definitions finite sets Sections AutomataTheory Doc

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

(x:A. P(x)) (x:A. P(x))
By: Sel 1 (Analyze 0)
Generated subgoal:

1 x:A. P(x)

About:
orallapplyuniversefunctionpropexists