Nuprl - Pf trivial_rel

(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1. name: relname()
2. r1: Term List
3. as: (LabelTerm) List
4. x:Label. unprime(apply_alist(as;x;x)) = x
5. i:
6. i < ||r1||

map(t.unprime(t);map(t.term_subst(as;t);r1))[i] = map(t.unprime(t);r1)[i]

By: RWW "map_select" 0 THEN Reduce 0 THEN Try ((Unfold `label` 0) THEN (Reduce 0) THEN Analyze THEN (RWW "map_select" 0) THEN (Reduce 0)) THEN Try ((BackThru Thm* t:Term, as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)) THEN (Try Trivial))

Generated subgoals:

None

About:

(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc