ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term. ds1 ds2 da1 da2 term_types(ds1;da1;de;t) term_types(ds2;da2;de;t)

UnivCD
THEN
TermInd -3
THEN
Unfold `term_types` 0
THEN
Reduce 0
THEN
Try (Fold `term_types` 0)
THEN
Try ((BackThru Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)) THEN SmAuto)
THEN
Try (BackThru Thm* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x))
THEN
Try ((BackThru Thm* c1,c2:Collection(T). c1 = c2 c1 c2) THEN RelRST)
THEN
Try Trivial

None

About: