0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maederops mkf : Logical -> Flag a;
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maeder getl : Flag a -> Logical
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maedervars x : Flag a; b : Logical
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maeder. mkf (getl x) = x
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maeder. getl (mkf b : Flag a) = b
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maederop sg : Flag a = mkf forall x, y : a . x = y
0fadccdf893d0551a8392ea0b9ad5d2f48885808Christian Maederop c : Logical = getl (sg : Flag a)