decide
c : Char
foo : ∀ {c : Prop} {t e : UInt32} [inst : Decidable c], 0 < t → 0 < e → 0 < if c then t else e :=
  fun {c} {t e} x x_1 x_2 =>
    match x, x_1, x_2 with
    | isTrue h, h_1, x => h_1
    | isFalse h, x, h_1 => h_1
⊢ 0 < UInt32.ofNatCore 3 utf8Size.proof_6
no goals