Level: Lib Thy Top: 2 1
Hypotheses:

  1. n :

  2. 0 < n

  3. T:. B:T . (f:(n - 1) T. g:T (n - 1). InvFuns((n - 1);T;f;g)) (t:T. Dec(B t)) (m:. f:m {t:T| B t} . g:{t:T| B t} m. InvFuns(m;{t:T| B t} ;f;g))

  4. T :

  5. B : T

  6. f : n T

  7. g : T n

  8. g o f = Id{n}

  9. f o g = Id{T}

  10. t:T. Dec(B t)

Conclusion:

m:. f:m {t:T| B t} . g:{t:T| B t} m. InvFuns(m;{t:T| B t} ;f;g)

Applied Tactic: (Assert f (n - 1) {t:T| g t < n - 1} ...a)
Generated subgoals:

1. f (n - 1) {t:T| g t < n - 1}

2. m:. f:m {t:T| B t} . g:{t:T| B t} m. InvFuns(m;{t:T| B t} ;f;g)