PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
1
T:Type, P,Q:(T
Prop). (
t:T. P(t)
Q(t))
({t:T| P(t) } ~ {t:T| Q(t) })
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
P:
T
Prop
3.
Q:
T
Prop
4.
t:T. P(t)
Q(t)
{t:T| P(t) } ~ {t:T| Q(t) }
About:
PropProp
t:T. P(t) 
Q(t)
{t:T| P(t) } ~ {t:T| Q(t) } T:Type, P,Q:(TProp). (t:T. P(t) Q(t)) 
({t:T| P(t) } ~ {t:T| Q(t) })PropPropt:T. P(t) Q(t) {t:T| P(t) } ~ {t:T| Q(t) }
