Arguing with sumbools

Question

I have the following definitions:

Variables Sd_pre : nat -> Prop.

Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
Admitted.

And the following are two of my hypotheses, which form a contradiction that I am trying to prove:

HeqSd1 : Sd1 = (if Sd_dec m then 0 else 1) 
T_tN_2 : Sd1 = 2

What I tried so far was proving this Lemma, but it didn't help because it was only for bools:

Lemma if_eq: forall d: bool, forall a b c: nat,  (a = if d then b else c) -> if d then a = b else a = c.
Proof.
intros.
induction d. auto. auto.
Qed.

If I try the same for sumbool, I get the error

The term "sumbool" has type "Prop -> Prop -> Set"
which should be Set, Prop or Type.

How do I get this Lemma for sumbool, or is there an easier way?

The same applies to this Lemma that I suppose I will also need to prove my original problem but has the same issue of being defined for bool instead of sumbool.

Lemma if_implies_or: forall a:bool, forall b c : Prop, (if a then b else c) -> b \/ c.
Proof.
intros.
induction a.
auto. auto.
Qed.

Answer 1

You can prove it like this:

Section foo.
  Variables Sd_pre : nat -> Prop.
  Definition Sd_dec : forall t, { Sd_pre t } + { ~Sd_pre t }.
  Admitted.

  Lemma the_contradiction m Sd1 :
    Sd1 = (if Sd_dec m then 0 else 1) ->
    Sd1 = 2 ->
    False.
  Proof.
    intros -> H. destruct (Sd_dec m). all: discriminate H.
  Qed.
End foo.

The main idea is to do a case distinction on which side of the if we are on. For this, we destruct Sd_dec m and are left with two cases, both of which are contradictory.

Note that the lemma statement for your if_eq would likely be something like

Lemma if_eq {T1 T2}: forall d: sumbool T1 T2, forall a b c: nat,  (a = if d then b else c) -> if d then a = b else a = c.

In particular, sumbool is not a type, but sumbool T1 T2 (with T1, T2 : Prop) is.