At:
rel arg typing2
1
1.
x: SimpleType
2.
r1: Term List
3.
i: 
4.
ds: Collection(dec())
5.
da: Collection(dec())
6.
st1: Collection(SimpleType)
7.
de: sig()
8.
rho: Decl
9.
s: {[[ds]] rho}
10.
s': {[[ds]] rho}
11.
e: {1of([[de]] rho)}
12.
a: [[st1]] rho
13.
tr: trace_env([[da]] rho)
14.
trace_consistent_rel(rho;da;tr.proj; < inl(x),r1 > )
15.
||r1|| = 2 
16.
x term_types(ds;st1;de;r1[0])
17.
x term_types(ds;st1;de;r1[1])
18.
i < ||r1||
x term_types(ds;st1;de;r1[i])
By:
CaseNat 0 `i'
THEN
Try Trivial
THEN
CaseNat 1 `i'
THEN
Try Trivial
Generated subgoals:
None
About:
