proposition: Lemma dio_rel_finite_conj n (R : nat -> (nat -> nat) -> Prop) : (forall i, i < n -> 𝔻R (R i)) -> 𝔻R (fun ν => forall i, i < n -> R i ν).
proof: Proof. intros H. apply fmap_reifier_t_default with (1 := df_true) in H. destruct H as (f & Hf). exists (df_mconj n f). abstract(intros v; rewrite df_mconj_spec; split; intros E i Hi; generalize (E _ Hi); apply Hf; trivial). Defined.
imports: Arith Nat ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums bounded_quantification)