A failing attempt to use https://github.com/coq/coq/pull/16868

ZifyTermTakeOne.v

From Coq Require Import Program.Basics.
From Coq Require        Program.Equality.
From Coq Require Import Vectors.Vector.
From Coq Require Import Logic.Eqdep.

Import VectorNotations.

Require Import Lia.
Require Import ZArith.
Require Import ZifyBool.
Import ZifyClasses.

Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n.
Notation bitvector n := (Vec n bool).

(* The exact definitions here aren't terribly important, so I've omitted them
   here for the sake of making this test case more minimal. *)
Definition bvToInt : forall w, bitvector w -> Z. Admitted.
Definition isBvult : forall w, bitvector w -> bitvector w -> Prop. Admitted.
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted.

Global Program Instance Inj_bv_Z w : InjTyp (bitvector w) Z :=
  { inj := bvToInt w
  ; pred := fun x => Z.le 0 x /\ Z.lt x (Z.pow 2 (Z.of_nat w))
  }.
Next Obligation.
Admitted.

Global Program Instance Rel_eq_bv w : BinRel (@eq (bitvector w)) :=
  { TR := @eq Z
  }.
Next Obligation.
Admitted.

Section S.

Variable w : nat.

Add Zify InjTyp (Inj_bv_Z w).
Add Zify BinRel (Rel_eq_bv w).

Lemma test_refl : forall (a : bitvector w), a = a.
Proof.
  (* Missing injection for type bitvector w *)
  Fail lia.
Admitted.

End S.