Nuprl - Pf rel_mng_lemma 1 2 1 1

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

1. ds: Collection(dec())
2. da: Collection(dec())
3. de: sig()
4. rho: Decl
5. st1: Collection(SimpleType)
6. e1: {1of([[de]] rho)}
7. s: {[[ds]] rho}
8. a: [[st1]] rho
9. tr: trace_env([[da]] rho)
10. l: Term List
11. u: Term
12. v: Term List
13. i:(||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i])
14. ls: SimpleType List
15. f: reduce(s,m. [[s]] rhom;Prop;ls)
16. ||ls|| = ||v||+1
17. i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i])

i:||v||. trace_consistent(rho;da;tr.proj;v[i])

By: Auto THEN InstHyp [i+1] -6 THEN Subst' ([u / v][(i+1)] = v[i]) -1

Generated subgoal:

1 18. i: ||v||
19. trace_consistent(rho;da;tr.proj;[u / v][(i+1)])
20. x,y:Term. x = y (x ~ y)
[u / v][(i+1)] = v[i]

About:

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