Nuprl - Pf auto2_lemma

1. T: Type
2. P: TProp
3. Q: TProp
4. t:T. P(t) Q(t)

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)

By: Witness Id

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)

About:

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)`