Nuprl - Pf member_col_subst2 2 2 3

(16steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: member col subst2 2 2 3

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))||

(p.2of(p))(as[i]) c(rel_primed_vars(r)[i])

By: Reduce 0 THEN Subst (rel_primed_vars(r)[i] ~ 1of(as[i])) 0 THEN Try (BackThruSomeHyp THEN (AllHyps (i.(Unfold `unzip` i) THEN (Reduce i) THEN (RWW "map_length_nat" i))))

Generated subgoal:

1 rel_primed_vars(r)[i] ~ 1of(as[i])

About:

(16steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc