Who Cites R safety?
R_safety	Def safetyR(E)(tr_1,tr_2) == tr_2 tr_1
	Thm* E:EventStruct. safetyR(E) (|E| List)(|E| List)Prop
carrier	Def |S| == 1of(S)
	Thm* S:Structure. |S| Type
iseg	Def l1 l2 == l:T List. l2 = (l1 @ l)
	Thm* T:Type, l1,l2:T List. l1 l2 Prop
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
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

Syntax:

safetyR(E)

has structure:

R_safety(E)

About: