WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc
Who Cites msg
content
eq?
msg_content_eq
Def cEQ(MS) == 1of(2of(MS))
Thm*
M:MessageStruct. cEQ(M)
DecidableEquiv
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
Syntax:
cEQ(MS)
has structure:
msg_content_eq(MS)
About:
WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc