# Arguing with sumbools

I have the following definitions:

Variables Sd_pre : nat -> Prop.

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



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.

• I was able to solve the original problem with induction tactic over Sd_dec m but I think an answer could still be interesting and valuable learning. Commented Jul 2 at 15:15

You can prove it like this:

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

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.