At:
trace consistent pred and p,q:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p q) trace_consistent_pred(rho;da;R;p) & trace_consistent_pred(rho;da;R;q)
By:
Unfolds [`pred`;`pred_and`;`trace_consistent_pred`] 0
THEN
Unfold `col_all` 0
THEN
RW ColMemberC 0
THEN
Try (BackThruSomeHyp THEN (Complete SimpConcl))
THEN
Analyze -1
THEN
EasyHyp
Generated subgoals:
p,q:Fmla, rho:Decl, da:Collection(dec()), R:(Label
Label
). trace_consistent_pred(rho;da;R;p 
q) 
trace_consistent_pred(rho;da;R;p) & trace_consistent_pred(rho;da;R;q)