proposition: Lemma decides_assumption : forall (P : Prop), P -> decides true P.
proof: Proof. simpl in *; intuition. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Notations