import "b.mm0";
import "c.mm0";

strict provable sort AA;
term termA1 (p: AA): AA; 
term termA2 : AA > BB > CC;