At: fusion weakening
E:TaggedEventStruct, I,J,P:TraceProperty(E). (J refines I) 
(I fuses P) (J fuses P)
By:
Unfolds [`trace_property`;`fusion_condition`;`tr_refines`] 0
THEN
Unfold `str_trace` 0
THEN
RepeatFor 2 BackThruSomeHyp
Generated subgoals:None
About:
