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