bool_neq_nat.v

Axiom bu : bool = unit.

Definition f : bool -> unit :=
  match bu in _ = b return bool -> b with
  | eq_refl => fun x => x
  end.

Definition g : unit -> bool :=
  match bu in _ = b return b -> bool with
  | eq_refl => fun x => x
  end.

Definition fg (x : bool) : g (f x) = x :=
  match bu as bu return (match bu in _ = b return b -> bool with
                   | eq_refl => fun x => x
                   end) ((match bu in _ = b return bool -> b with
                       | eq_refl => fun x => x
                       end) x) = x with
  | eq_refl => eq_refl
  end.

Goal False.
pose proof (fg false) as H1.
pose proof (fg true) as H2.
destruct (f _).
destruct (f _).
rewrite H2 in H1.
discriminate.
Qed.