PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 6 1 1 1 1 1 2 1 1 1 1 1 1 2

1. n:
2. 0 < n
3. T: Type
4. R: TProp
5. f: nT
6. Bij(n; T; f)
7. t:T. Dec(R(t))

t:{t:T| t = f(n-1) }. Dec(R(t))

By: Analyze 0

Generated subgoal:

18. t: {t:T| t = f(n-1) }
Dec(R(t))


About:
allsetequalapplysubtractnatural_number
intless_thanuniversefunctionprop