* Some very basic checking of a proposition parameterised on a modality
prop A(a) = [a]F;
prop A;
cp (c.0, A(b));
cp (b.0, A(b));
cp (b.0, A({a,b}));
cp (a.0, A({a,b}));
set AS = {a,b};
cp (c.0, A(AS));
cp (b.0, A(AS));
cp (b.0, A(-AS));
cp (a.0, A(-AS));
cp (a.0+c.0, A(-AS));
cp (b.0, A(-));
cp (b.0, A(-b));
cp (b.0, A(-a));