At: member col subst21 1. c: LabelCollection(Term) 2. r: rel() 3. r': rel() 4. as: (LabelTerm) List 5. 1of(unzip(as)) = rel_vars(r) 6. i:. i < ||as|| 2of(as[i]) c(1of(as[i])) 7. r' = rel_subst(as;r)
||2of(unzip(as))|| = ||map(c;rel_vars(r))|| By: All (i.(Unfold `unzip` i) THEN (Reduce i) THEN (RWW "map_length_nat" i))
THEN
SubstFor rel_vars(r) 0
THEN
RWW "map_length_nat" 0 Generated subgoals:
Collection(Term)
Term) List
i:
. i < ||as|| 
2of(as[i]) 
c(1of(as[i]))
||2of(unzip(as))|| = ||map(c;rel_vars(r))|| 
i.(Unfold `unzip` i) THEN (Reduce i) THEN (RWW "map_length_nat" i))