proposition: Lemma decides_dec_eq {A} : forall (A_eqb : A -> A -> bool) (A_eqb_sound : forall a a', a = a' <-> A_eqb a a' = true) (a a' : A), decides (A_eqb a a') (a = a').
proof: Proof. simpl in *; intros; pose proof (A_eqb_sound a a'); destruct (A_eqb a a'); simpl; intuition. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations