bool
2
jlc
Sections
Support(jlc)
Doc
Def
true
== inl(
)
is mentioned by
Thm*
P:
. P
P = true
[assert_iff_btrue_rw]
Thm*
P:
. P
P = true
[assert_iff_btrue]
In prior sections:
bool
1
bool
2
jlc
Sections
Support(jlc)
Doc
P:
. P 
P = true
P:. P P = true == inl(
)
P:. P P = trueP:. P P = true