discrete
jlc
Sections
Support(jlc)
Doc
Def
S
T ==
x:S. x
T
is mentioned by
Thm*
{T=
}
(T
T
)
[discrete_equality_inc]
In prior sections:
int
1
discrete
jlc
Sections
Support(jlc)
Doc
} 
(T
T
) T == 
x:S. x 
T
} (TT)