Level: Lib Thy Top: 1 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:

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

Applied Tactic: (Unfold `inv_funs` 0 THEN Unfold `inv_funs` 5 THEN D 0 ...)
Generated subgoals:

1. f o g = Id{{t:T| B t} }