At: P tag by msg safety E:TaggedEventStruct. safetyR(E) preserves Tag-by-msg(E) By: Unfolds [`preserved_by`;`R_safety`] 0
THEN
Reduce 0
THEN
Try (Fold `trace_property` 0)
THEN
Inst
Thm*l1,l2:T List.
l1 l2 ||l1||||l2|| & (i:. i < ||l1|| l1[i] = l2[i])
[|E|;y;x]
THEN
SimpHyp -1
THEN
ExRepD
THEN
MoveToHyp 0 -4 Generated subgoal: