PrintForm Definitions exponent Sections AutomataTheory Doc

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

False
By: Unfold `inject` 6
Generated subgoal:

16. a1,a2:n. f(a1) = f(a2) a1 = a2
7. t:T. Dec(R(t))
8. b: T
9. b = f(n-1)
10. a: n
11. f(a) = b
12. a1: (n-1)
13. f(a1) = f(n-1)
False

About:
falseintless_thannatural_numberuniversefunction
propallapplyequalsubtract