proposition: Theorem finite_t_model ls : finite_t_upto funs (R ls).
proof: Proof. Proof using y Hsyms HY HX2 HX1. induction ls as [ | s ls IH ]. + exists ((fun _ _ => y) :: nil). intros f; exists (fun _ _ => y); split; simpl; auto. intros ? []. + destruct IH as (m & Hm). destruct fun_finite_t_upto with (vec X (ar s)) Y as (l & Hl); auto. exists (map (fun p => fun_combine (fst p) (snd p)) (list_prod l m)). intros f. destruct (Hl (f s)) as (f' & H1 & H2). destruct (Hm f) as (g & H3 & H4). exists (fun_combine f' g); split. * apply in_map_iff; exists (f',g); split; auto. apply list_prod_spec; simpl; auto. * intros s' [ <- | Hs ] v. - red in H2; rewrite H2. unfold fun_combine. destruct (Hsyms s s) as [ E | [] ]; auto. rewrite (UIP_dec Hsyms E eq_refl); auto. - unfold fun_combine. destruct (Hsyms s s') as [ E | D ]. ++ subst; cbn; apply H2. ++ apply H4; 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)