proposition: Lemma decides_eq_refl {A} : forall (a : A), decides true (a = a).
proof: Proof. simpl in *; intuition. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations