Kruskal-Trees v1.1

Some additional features:

• shortlex order on undecorated rose trees rtree;
• compatibility layer for Arith lemmas using lia;
• decidability of equality for decorated rose trees dtree and vtree;
• extensional decidability for vectors.