PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 2 1 1 1 1 1
1. T: Type
2. R: TProp
3. n:
4. f:(nT). Bij(n; T; f)
5. t:T. Dec(R(t))

(f:(nT). Bij(n; T; f)) & (t:T. Dec(R(t)))
By: Analyze 0
Generated subgoals:

None

About:
andexistsfunctionnatural_numberallapplyuniverseprop