At: rel mng 2 lemma 1 2 1 1 1
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. s': {[[ds]] rho}
9. a: [[st1]] rho
10. tr: trace_env([[da]] rho)
11. l: Term List
12. u: Term
13. v: Term List
14. 
i:
(||v||+1). trace_consistent(rho;da;tr.proj;[u / v][i])
15. ls: SimpleType List
16. f: reduce(
s,m. [[s]] rho
m;Prop;ls)
17. ||ls|| = ||v||+1 
18. i:. i < ||v||+1 
ls[i] term_types(ds;st1;de;[u / v][i])
19. i: ||v||
20. trace_consistent(rho;da;tr.proj;[u / v][(i+1)])
21. x,y:Term. x = y (x ~ y)
[u / v][(i+1)] = v[i]
By: RWO "select_cons_tl" 0
Generated subgoals:None
About:
