Nice idea, but it breaks quite quickly (still). Tried to see if Cosette can prove equivalence of these two queries:

    /* define schema s1, 
       here s1 can contain any number of attributes, 
       but it has to at least contain integer attributes 
       x and y */
    schema s1(x:int, ya:int, ??);
    
    schema s2(yb:int, ??);        -- define schema s2
    
    table a(s1);            -- define table a using schema s1
    table b(s2);            -- define table b using schema s1
    
    query q1                -- define query q1 on tables a and b
    `select distinct x.x as ax from a x, b y
     where x.ya = y.yb`;
    
    query q2                -- define query q2 likewise
    `select x.x as ax from a x, a y, b z 
     where x.x = y.x and x.ya = z.yb
     union select 1 as ax from a x where 1 = 0`;
    
    verify q1 q2;           -- does q1 equal to q2?

Got a syntax error:

    Syntax Error. 
    ERROR: (line 19, column 8):
    unexpected "s"
    expecting "--" or "/*"

There are many other bugs up to the point where this is not really usable.