discrete
jlc
Sections
Support(jlc)
Doc
Def
P & Q == P
Q
is mentioned by
Thm*
eq:{T=
}. (
x,y:T. eq(x,y)
x = y) & eq
T
T
[discrete_equality_properties]
In prior sections:
core
int
1
bool
1
discrete
jlc
Sections
Support(jlc)
Doc
eq:{T=
}. (x,y:T. eq(x,y) 
x = y) & eq 
T
T
Q
eq:{T=}. (x,y:T. eq(x,y) x = y) & eq TT