From 1cbda4875239544ea86f5f106151116079dbf195 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 29 Nov 2018 09:49:30 +0100
Subject: [PATCH] Type class version of `elem_of` for lists.

---
 theories/base.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 2a96208b..3043b473 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -129,6 +129,13 @@ Existing Class TCForall2.
 Existing Instance TCForall2_nil.
 Existing Instance TCForall2_cons.
 
+Inductive TCElemOf {A} (x : A) : list A → Prop :=
+  | TCElemOf_here xs : TCElemOf x (x :: xs)
+  | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
+Existing Class TCElemOf.
+Existing Instance TCElemOf_here.
+Existing Instance TCElemOf_further.
+
 Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
 Existing Instance TCEq_refl.
-- 
GitLab