Nuprl - Pf assert_subst_mentions

1. as: (LabelTerm) List
2. u: LabelTerm
3. v: (LabelTerm) List
4. subst_mentions_trace(v) (i:||v||. mentions_trace(2of(v[i])))

subst_mentions_trace([u / v]) (i:(||v||+1). mentions_trace(2of([u / v][i])))

By: Unfold `subst_mentions_trace` 0 THEN Reduce 0 THEN Fold `subst_mentions_trace` 0 THEN RW assert_pushdownC 0

Generated subgoal:

1 mentions_trace(2of(u)) subst_mentions_trace(v) (i:(||v||+1). mentions_trace(2of([u / v][i])))

About: