a b c✝ d : Prop
p : ?m.27950
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
this : t
⊢ t
a b c✝ d : Prop
p : ?m.27950
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
⊢ t
have := if_pos hc ▸ h
no goals
a b c✝ d : Prop
p : ?m.27950
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
this : t
⊢ t
exact this