At:
rel mng 2 wf
1
1
2
1
1
2
1
1.
y: Label
2.
r1: Term List
3.
ds: Collection(dec())
4.
da: Collection(dec())
5.
de: sig()
6.
rho: Decl
7.
st1: Collection(SimpleType)
8.
e1: {1of([[de]] rho)}
9.
e2: l:Label
reduce(
s,m. [[s]] rhom;Prop;de.rel(l))
10.
s: {[[ds]] rho}
11.
s': {[[ds]] rho}
12.
a: [[st1]] rho
13.
tr: trace_env([[da]] rho)
14.
trace_consistent_rel(rho;da;tr.proj; < inr(y),r1 > )
15.
l: Term List
16.
r1 = l
17.
||de.rel(y)|| = ||l|| 
18.
i:. i < ||l|| 
(de.rel(y))[i] term_types(ds;st1;de;l[i])
19.
f: reduce(s,m. [[s]] rhom;Prop;de.rel(y))
20.
e2.y = f
21.
i: ||l||
trace_consistent(rho;da;tr.proj;l[i])
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:
