PrintForm Definitions exponent Sections AutomataTheory Doc

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

1. n:
2. 0 < n
3. T: Type
4. R: TProp
5. f: nT
6. Inj(n; T; f)
7. R(f(n-1))
8. t: T
9. R(t)
10. a: n
11. f(a) = t
12. a = n-1 n

t = f(n-1)

By: Analyze 0

Generated subgoal:

113. t = f(n-1)
False


About:
equalapplysubtractnatural_numberint
less_thanuniversefunctionpropfalse