PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 1 1 1 2 2

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

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

By: Unfold `inv_funs` 0

Generated subgoal:

1 Id o Id = Id & Id o Id = Id


About:
setapplyuniversefunctionpropallandequal