EnvironmentStructsV0🍃 Equality_witness.v🍃 Equality_witness.vEnvironmentGitlab 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.