At: covers pred lemma2 1 2 1 1 1 1 1 2 1 1 1
1. r: rel()
2. I: Collection(rel())
3. A: ioa{i:l}()
4. a: Label
5. r 
I
6. 
x:Label. (x rel_vars(r)) 
covers_var(A;x)
7. x: Label
8. (x rel_primed_vars(r))
(x rel_vars(r))
By: BackThru
Thm* r:rel(), x:Label. (x rel_primed_vars(r)) (x rel_vars(r))
Generated subgoals:None
About:
