At: covers pred lemma2 1 1
1. r: rel()
2. I: Collection(rel())
3. A: ioa{i:l}()
4. a: Label
5. 
x:Label. (
r:rel(). r 
I & rel_mentions(r;x)) 
covers_var(A;x)
6. r I
x:Label. rel_mentions(r;x) covers_var(A;x)
By:
Auto
THEN
BackThruSomeHyp
THEN
AutoInstConcl []
Generated subgoals:None
About:
