PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
1
1
1
2
2
1.
T:
Type
2.
P:
T
Prop
3.
Q:
T
Prop
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: