Who Cites R send enabled?
R_send_enabled	Def send-enabledR(E)(L_1,L_2) == x:|E|. (is-send(E)(x)) & L_2 = (L_1 @ [x])
	Thm* E:EventStruct. send-enabledR(E) (|E| List)(|E| List)Prop
append	Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs) T List
carrier	Def |S| == 1of(S)
	Thm* S:Structure. |S| Type
event_is_snd	Def is-send(E) == 1of(2of(2of(2of(2of(E)))))
	Thm* E:EventStruct. is-send(E) |E|
assert	Def b == if b True else False fi
	Thm* b:. b Prop
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))

Syntax:

send-enabledR(E)

has structure:

R_send_enabled(E)

About: