(LabelTerm) List

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

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

x@0:Label. (x@0 rel_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)))

x term_types(ds;da;de;term_subst(as;r1[0])) & x term_types(ds;da;de;term_subst(as;r1[1]))

Analyze 0
THEN
BackThru Thm* t:Term, s:SimpleType, as:(LabelTerm) List, ds:Collection(dec()) , da:Collection(SimpleType), de:sig(). s term_types(ds;da;de;t) (x:Label. (x term_vars(t)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) s term_types(ds;da;de;term_subst(as;t))
THEN
InstHyp [x1] -6
THEN
Try BackThruSomeHyp
THEN
Try ((Folds [`relname_eq`;`mk_rel`] 0) THEN (RWW "member_rel_vars" 0) THEN (Reduce 0))

1	12. x1: Label 13. (x1 term_vars(r1[0])) 14. t: SimpleType 15. mk_dec(x1, t) ds i:. i < ||r1|| & (x1 term_vars(r1[i]))
2	12. x1: Label 13. (x1 term_vars(r1[1])) 14. t: SimpleType 15. mk_dec(x1, t) ds i:. i < ||r1|| & (x1 term_vars(r1[i]))

About: