At:
rel mng wf
1
1
1
3
1.
x: SimpleType
2.
r1: Term List
3.
ds: Collection(dec())
4.
da: Collection(dec())
5.
de: sig()
6.
rho: Decl
7.
st1: Collection(SimpleType)
8.
e: {[[de]] rho}
9.
s: {[[ds]] rho}
10.
a: [[st1]] rho
11.
tr: trace_env([[da]] rho)
12.
trace_consistent_rel(rho;da;tr.proj; < inl(x),r1 > )
13.
l: Term List
14.
r1 = l
15.
||l|| = 2 
16.
x term_types(ds;st1;de;l[0])
17.
x term_types(ds;st1;de;l[1])
18.
i: 
||l||
19.
i = 0
20.
i = 1
trace_consistent(rho;da;tr.proj;l[1])
By:
AllHyps (
h.(Unfold `trace_consistent_rel` h) THEN (Reduce h) THEN (MoveToHyp -1 h) THEN (SubstFor r1 -2) THEN (BackThru -2))
Generated subgoals:
None
About:
