At: member col subst2 2 2 2
1. c: LabelCollection(Term)
2. r: rel()
3. r': rel()
4. as: (LabelTerm) 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))||
i < ||rel_primed_vars(r)||
By: SubstFor rel_primed_vars(r) 0
Generated subgoal:1 | i < ||1of(unzip(as))|| |
About: