(LabelTerm) List

x term_types(ds;da;de;r1[0])

x term_types(ds;da;de;r1[1])

x@0:Label. (x@0 rel_primed_vars( < inl(x),r1 > )) (t:SimpleType. mk_dec(x@0, t) ds t term_types(ds;da;de;apply_alist(as;x@0;x@0)))

||map(t.term_subst2(as;t);r1)|| = 2

x term_types(ds;da;de;map(t.term_subst2(as;t);r1)[0]) & x term_types(ds;da;de;map(t.term_subst2(as;t);r1)[1])

1	11. ||r1|| = 2 x term_types(ds;da;de;term_subst2(as;r1[0])) & x term_types(ds;da;de;term_subst2(as;r1[1]))

About: