proposition: Theorem finite_t_valuations ln : finite_t_upto _ (R ln).
proof: Proof. Proof using x HX1. induction ln as [ | n ln IH ]. + exists ((fun _ => x)::nil). intros f; exists (fun _ => x); split; simpl; auto. intros ? []. + destruct HX1 as (l & Hl). destruct IH as (m & Hm). exists (map (combine n) (list_prod l m)). intros f. destruct (Hm f) as (g & H1 & H2). exists (combine n (f n,g)); split. * apply in_map_iff; exists (f n,g); split; auto. apply list_prod_spec; auto. * intros n' [ <- | Hn' ]. - unfold combine. destruct (eq_nat_dec n n) as [ | [] ]; auto. - unfold combine. destruct (eq_nat_dec n n') as [ E | D ]; 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)