At: term mng equal 1 2 2 1
1. ds: Collection{i}(dec())
2. da: Collection{i}(dec())
3. st: Collection{i}(SimpleType)
4. de: sig()
5. rho: Decl{i}
6. e1: {1of(sig_mng{i:l}
(de; rho))}
7. s1: {[[ds]] rho}
8. s2: {[[ds]] rho}
9. a: [[st]] rho
10. tr: trace_env([[da]] rho)
11. u: Term
12. u1: Term
Type{i'}
13. w: u:{v:Term| u1(v) }
t:SimpleType.
trace_consistent(rho;da;tr.proj;u) 
(x:Label. (x 
term_vars(u)) s1.x = s2.x)
t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho
14. y1: {v:Term| u1(v) }
15. y2: {v:Term| u1(v) }
16. t: SimpleType
17. trace_consistent(rho;da;tr.proj;y1 y2)
18. x:Label. (x term_vars(y1) @ term_vars(y2)) s1.x = s2.x
19. a1: SimpleType
20. a1 term_types(ds;st;de;y2)
21. a1t term_types(ds;st;de;y1)
22. [[y1]] e1 s1 a tr = [[y1]] e1 s2 a tr [[a1t]] rho
trace_consistent(rho;da;tr.proj;y2)
By: AllHyps
(
h.
(RepeatFor 2 (ParallelOp h)) THEN (ParallelOp -1) THEN (Reduce 0) THEN (RW assert_pushdownC 0)
THEN
(Complete SimpConcl))
Generated subgoals:None
About:
