Selecting a way to write optional decidable Prop

Stream: general

[Naruyoko]

I'm trying to write a property on op : option Prop which states that the Prop it contains when it is some variant is decidable, and came up with several ways:

@[reducible]
def optional_decidable₁ (op : option Prop) : Prop :=
fact $ true <| (nonempty ∘ decidable) <$> op

@[reducible]
def optional_decidable₂ (op : option Prop) : Prop :=
fact $ option.cases_on op true (λ p, nonempty (decidable p))

@[reducible]
def optional_decidable₃ (op : option Prop) : Prop :=
fact $ match op with | none := true | (some p) := nonempty (decidable p) end

@[reducible]
def optional_decidable₄ : option Prop → Prop :=
fact ∘ option.elim true (nonempty ∘ decidable)

(I made it a type class to be able to infer decidable instance when using e.g. option.get or option.lhoare. The intended use is to automate decidable inference of predicates on an option that use the contained value.)
The definitions should be equivalent, but is there a practical reason to choose one over the other?

[Naruyoko]

(I'm also having trouble extracting the decidable instance, as cases and similar seem to produce a wrong sort)

[Yury G. Kudryashov]

You can't put your typeclass in Prop, then computably extract a decidable instance because the latter contains data.

[Naruyoko]

I see

[Naruyoko]

My current end goal for doing this is to be able to write things like "option (is none or | is not none and) its contained value satisfies a predicate" and "two options are some and the contained values satisfies a relation," and I figured using lhoare and map is a good way to do this. However, I am starting to think the simpler way is to just use option.elim, define a single decidable instance on it, and pass an option of a product when I need to check two values.