proposition: Lemma decide_decideP {P:Prop }`{Decidable P} {R:Type} (a b : R) : (if (decide P) then a else b) = (if (decideP P) then a else b).
proof: Proof. symmetry. unfold decide. destruct (decideP P). - rewrite Decidable_complete; auto. - rewrite Decidable_sound_alt; auto. Qed.
imports: Coq.Classes.DecidableClass