proposition: Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) : (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
proof: Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
imports: stdpp(options)