proposition: Lemma Decidable_sound_alt : forall P (H : Decidable P), ~ P -> Decidable_witness = false.
proof: Proof. intros. destruct Decidable_witness eqn:Heqe; trivial. apply Decidable_spec in Heqe. contradiction. Qed.
imports: Coq.Arith.Compare_dec Fiat.Common.Coq__8_4__8_5__Compat