At: member col subst2 2 2 3 1 1 2
1. c: Label
Collection(Term)
2. r: rel()
3. r': rel()
4. as: (Label
Term) List
5. 1of(unzip(as)) = rel_primed_vars(r)
6. 
i:
. i < ||as|| 
2of(as[i]) 
c(1of(as[i]))
7. r' = rel_subst2(as;r)
8. i:
9. i < ||2of(unzip(as))||
10. rel_primed_vars(r) = 1of(unzip(as))
11. x: Label List
12. y: Label List
13. x = y
14. SQType(Label List)
x ~ y
By:
Unfold `guard` 0
THEN
Unfold `sq_type` -1
THEN
BackThruSomeHyp
Generated subgoals:None
About:
