##]
nqed.
ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##10: #H; napply (λx:P.x)
##]
nqed.
ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##10: #H; napply (λx:P.x)