apply bool_ind (\lambda b:bool.
(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow m-(S n)
apply bool_ind (\lambda b:bool.
(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow m-(S n)