proposition: Fact mb_is_tuple_inj t n (v w : vec _ n) p : t ≋ ⦉v⦊ -> t ≋ ⦉w⦊ -> vec_pos v p ≈ vec_pos w p.
proof: Proof. Proof using mb_axiom_ext. intros H1 H2; revert t w H1 H2 p; induction v as [ | n x v IHv ]; intros t w. + intros _ _ p; invert pos p. + vec split w with y. intros (p & H1 & H2) (q & H3 & H4). destruct (mb_is_opair_inj H1 H3) as (E1 & E2). apply mb_is_tuple_congr with (1 := E2) in H2. specialize (IHv _ _ H2 H4). intros j; invert pos j; auto. Qed.
imports: List Arith Nat Lia Max Wellfounded Coq.Setoids.Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations fol_ops fo_sig fo_terms fo_logic)