Skip to main content

🍃 Equality_witness.v

Environment

Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive eq : Set :=
| Refl : eq.

Parameter t : (a : Set), Set.

Parameter make : {a : Set}, unit t a.

Parameter eq_value : {a b : Set}, t a t b option eq.

Parameter hash_value : {a : Set}, t a int.