Definition fb (x : bool) : Set := nat.
Definition fn (x : nat) : Set := nat.
(* New decision procedure because bool_dec is annoying. *)
Lemma bool_true_false (b : bool) : {b = true} + {b = false}.
destruct b.
left. reflexivity.
right. reflexivity.
Defined.
(* Print bool_true_false. *)
Definition bool_or_nat (b : bool) := if b then bool else nat.
(* Use eq_rect to convert "x : bool_or_nat b" to "x : bool_or_nat true" using "b = true" *)
Definition depx
(b : bool)
(x : bool_or_nat b)
(y : match bool_true_false b with
| left H => fb (eq_rect b bool_or_nat x true H)
| right H => fn (eq_rect b bool_or_nat x false H)
end)
:= 0.