structure O (c : False = False) where
  m : Prop