proposition: Lemma decides_3_True (A B : Type) (C : B -> Type) : refine {b' | decides b' (A -> forall b : B, C b -> True)}%comp (ret true).
proof: Proof. computes_to_econstructor; computes_to_inv; subst; simpl; auto. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics