proposition: Fact hfs_tuple_pow n v t : ∅ ∈ t -> hfs_transitive t -> (forall p, vec_pos v p ∈ t) -> @hfs_tuple n v ∈ iter hfs_pow t (2*n).
proof: Proof. intros Ht1 Ht2. induction v as [ | x n v IHv ]; intros Hv. + simpl; auto. + replace (2*S n) with (2*n+2) by lia; rewrite iter_plus. simpl hfs_tuple; apply hfs_opair_pow. * apply hfs_iter_pow_le with 0; try lia; auto. simpl; apply (Hv pos0). * apply IHv; auto. intro; apply (Hv (pos_nxt _)). Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops membership btree)