At: covers pred lemma2 1 2 1 1 1 1 1 2 1 2 1 1 2 2 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))
9. fr: frame()
10. fr A.frame
11. fr.var =
x
12. a:Label. (a fr.acts) (
ef:eff(). ef A.eff & ef.kind = a & ef.smt.lbl = x)
13. 
(a fr.acts)
(e:eff(). e A.eff & e.kind = a & mk_smt(fr.var, fr.var, fr.typ) = e.smt)
(f:frame().
f A.frame & 
a f.acts & mk_smt(fr.var, fr.var, fr.typ) = mk_smt(f.var, f.var, f.typ))
By:
Sel 2 (Analyze 0)
THEN
AutoInstConcl []
Generated subgoal:
About:
