PrintForm Definitions finite sets Sections AutomataTheory Doc

At: not dec is dec

A:Type, P:(AProp). (x:A. P(x) P(x)) & (x:A. P(x)) (x:A. P(x)) (x:A. P(x)) (x:A. P(x))
By: UnivCD
Generated subgoal:

11. A: Type
2. P: AProp
3. (x:A. P(x) P(x)) & (x:A. P(x)) (x:A. P(x))
(x:A. P(x)) (x:A. P(x))

About:
alluniversefunctionpropimplies
andorapplyexists