WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites prop
and?
prop_and
Def (P
Q)(L) == P(L) & Q(L)
Thm*
T:Type, P,Q:(T
Prop). (P
Q)
T
Prop
Syntax:
P
Q
has structure:
prop_and(P; Q)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Q)(L) == P(L) & Q(L)
T:Type, P,Q:(T
Prop). (P Q) 
TProp Q)(L) == P(L) & Q(L)T:Type, P,Q:(TProp). (P Q) TProp Q
