At: rel mng 2 lemma 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. 
i:
0. trace_consistent(rho;da;tr.proj;nil[i])
ls:SimpleType List, f:reduce(
s,m. [[s]] rho
m;Prop;ls).
||ls|| = 0 
& (i:. i < 0 
ls[i] term_types(ds;st1;de;nil[i])) f Prop
By:
InductionOnList
THEN
Reduce 0
THEN
ExRepD
Generated subgoals:None
About:
