a b c✝ d : Prop
p : ?m.28021
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
this : e
⊢ e
a b c✝ d : Prop
p : ?m.28021
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
⊢ e
have := if_neg hnc ▸ h
no goals
a b c✝ d : Prop
p : ?m.28021
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
this : e
⊢ e
exact this