PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 0 1 1 1

1. T: Type
2. P: TProp
3. x:T. Dec(P(x))
4. (x:T. P(x)) (x:T. P(x))

(x:T. P(x)) (x:T. P(x))

By: Analyze 4

Generated subgoals:

14. x:T. P(x)
(x:T. P(x)) (x:T. P(x))
24. (x:T. P(x))
(x:T. P(x)) (x:T. P(x))


About:
orallapplyuniversefunctionpropexists