Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. B : T

  3. f : 0 T

  4. g : T 0

  5. InvFuns(0;T;f;g)

  6. 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: (InstConcl [0;f;g] ...a)
Generated subgoals:

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