have hite' := notNotElim hite
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
⊢ ¬c ∨ a
case a
c a b : Prop
h : Decidable c
hite : ¬¬if c then a else b
hite' : if c then a else b
⊢ ¬c ∨ a