PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
1
1
1
2
2
1
1
1
1
1.
T:
Type
2.
P:
T
Prop
3.
Q:
T
Prop
4.
t:T. P(t)
Q(t)
Id = Id & Id = Id
By:
Unfold `tidentity` 0
Generated subgoal:
1
Id = Id
{t:T| P(t) }
{t:T| P(t) } & Id = Id
{t:T| Q(t) }
{t:T| Q(t) }
About:
Id = Id 
{t:T| P(t) }
{t:T| P(t) } & Id = Id {t:T| Q(t) }{t:T| Q(t) }PropProp
t:T. P(t) 
Q(t) Id = Id & Id = Id Id = Id {t:T| P(t) }{t:T| P(t) } & Id = Id {t:T| Q(t) }{t:T| Q(t) }
