0 | module Decidable.Decidable.Extra1

2 | import public Decidable.Decidable

4 | public export

5 | toWitness : {prf : Dec a} -> (0 _ : IsYes prf) -> a

6 | toWitness {prf = Yes prf} x = prf