combine_odd_even' : (podd, peven : Nat -> Type) -> (Nat -> Type)
combine_odd_even' podd peven n with (evenb n)
combine_odd_even' podd peven n | False = podd n
combine_odd_even' podd peven n | True = peven n

combine_odd_even_intro : (n : Nat) ->
(oddb n = True -> podd n) ->
(oddb n = False -> peven n) ->
combine_odd_even' podd peven n
combine_odd_even_intro k f g with (evenb k)
combine_odd_even_intro k f g | False = f Refl
combine_odd_even_intro k f g | True = g Refl