a,z:
, n:
, s:({a...z}
{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (n<i
(x:{a...z}. (s(?) {to n} 
h {to n'})(x,i) = h(i)))n:, f:({1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
f':({n+1...n'}Peg), i:{1...n'}.
Thm* (n<i
(f {to n} f' {to n'})(i) = f'(i))