* 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));