At: covers pred rel member A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r) By: Unfolds [`covers_pred`;`covers_rel`] 0
THEN
Try (Fold `pred` 0)
THEN
BackThruSomeHyp
THEN
Unfold `pred_mentions` 0
THEN
AutoInstConcl []
THEN
Fold `pred` 0 Generated subgoals:
A:ioa{i:l}(), I:Fmla, r:rel(). r 
I 
covers_pred(A;I)