Inductive world : Type := MsgFromRealSatoshi | MsgFromFakeSatoshi.

Definition possible_world (w v:world) := True.

Definition msg_from_satoshi (w:world) : Prop :=
  match w with
  | MsgFromRealSatoshi => True
  | MsgFromFakeSatoshi => False
  end.

Definition know (p:world -> Prop) (w:world) : Prop :=
  forall v:world, possible_world w v -> p v.

Definition neg (p:world -> Prop) (w:world) : Prop := ~ p w.

Theorem not_know_not_real_satoshi : forall w, neg (know (neg msg_from_satoshi)) w.
intros w H.
exact (H MsgFromRealSatoshi I I).
Qed.

Theorem not_know_real_satoshi : forall w, neg (know msg_from_satoshi) w.
intros w H.
exact (H MsgFromFakeSatoshi I).
Qed.