proposition: Theorem pred_finite_t_upto : finite_t_upto { p : X -> Prop & forall x, decidable (p x) } (fun p q => prop_ext (projT1 p) (projT1 q)).
proof: Proof. Proof using HX2 HX1. destruct fun_finite_t_upto with X bool as (l & Hl); auto. exists (map bool_prop l). intros (p & Hp). destruct (Hl (fun x => if Hp x then true else false)) as (f & H1 & H2). exists (bool_prop f); split. + apply in_map_iff; exists f; auto. + simpl; intros x; red in H2. rewrite <- H2. destruct (Hp x); split; auto; discriminate. 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)