Level: Lib Thy Top: 2
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. InvFuns(n;T;f;g)

  9. 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: (Unfold `inv_funs` 8 THENM GenRepD ...a)
Generated subgoals:

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