proposition: Fact hfs_tuple_spec n v w : @hfs_tuple n v = hfs_tuple w <-> v = w.
proof: Proof. split. + induction n as [ | n IHn ] in v, w |- *. * vec nil v; vec nil w; auto. * vec split v with x; vec split w with y; simpl. rewrite hfs_opair_spec; intros (-> & H); f_equal; revert H; auto. + intros ->; auto. 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)