At:
trivial-arrows
1
1
1
1
1
1.
k: 
2.
L:
List
3.
n:
.
k-1
n

(
G:({s:(
n List)| ||s|| = k
& (
x,y:
||s||. x < y 
s[x] < s[y]) }

||L||).
c:
||L||, f:(
L[c]

n).
increasing(f;L[c])
& (
s:
L[c] List. ||s|| = k

(
x,y:
||s||. x < y 
s[x] < s[y]) 
G(map(f;s)) = c))
4.
s:
(k-1) List
5.
||s|| = k
6.
x,y:
||s||. x < y 
s[x] < s[y]
Inj(
k;
(k-1);
x.s[x])
By:
BackThru
Thm*
k,m:
, f:(
k

m). increasing(f;k) 
Inj(
k;
m; f)
THEN
Analyze 0
THEN
Reduce 0
THEN
EasyHyp
Generated subgoals:
None
About: