At: decidable ex int seg 1 1 1 2 2 2 1 1
1. i: 
2. j:
3. F: {i..j
}
Prop
4. 
k:{i..j}. Dec(F(k))
5. i
j
6. n: {...j-1}
7. in
8. 
(
k:{(n+1)..j}. F(k))
9. F(n)
10. k: {n..j}
11. F(k)
12. k = n
False
By:
Assert (k = n)
THEN
HypSubst -1 11
Generated subgoals:None
About:
