PrintForm Definitions exponent Sections AutomataTheory Doc

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

g:({t:T| Q(t) }{t:T| P(t) }). InvFuns({t:T| P(t) }; {t:T| Q(t) }; Id; g)
By: Witness Id
Generated subgoals:

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

About:
existsfunctionsetapplyuniversepropallmember