Level: Lib Thy Top: 1 1
Hypotheses:

  1. T :

  2. P : T

  3. Q : T

  4. t:T. P t Q t

Conclusion:

f:{t:T| P t} {t:T| Q t} . g:{t:T| Q t} {t:T| P t} . InvFuns({t:T| P t} ;{t:T| Q t} ;f;g)

Applied Tactic: With Id (D 0) THENA Auto
Generated subgoals:

1. Id {t:T| P t} {t:T| Q t}

2. g:{t:T| Q t} {t:T| P t} . InvFuns({t:T| P t} ;{t:T| Q t} ;Id;g)