proposition: Fact decidable_bool_eq P : (decidable P -> { Q : bool | P <-> Q = true }) * ({ Q : bool | P <-> Q = true } -> decidable P).
proof: Proof. split. + intros H; exists (if H then true else false); destruct H; split; auto; discriminate. + intros (Q & HQ); destruct Q; [ left | right ]; rewrite HQ; auto. Qed.
imports: List Arith Bool Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops)