PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 0 1 1 1 2 1 1

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

P(x)

By: Witness3 x

Generated subgoal:

13. (x:T. P(x))
4. x: T
5. Dec(P(x))
P(x)


About:
applyuniversefunctionpropallexists