inductive Record (α : Type u) : List String → Type u

• nil {α : Type u} : Record α []
• cons {α : Type u} {keys : List String} (key : String) : ¬key ∈ keys → α → Record α keys → Record α (key :: keys)

inductive Mem {α : Type u} {keys : List String} : Record α keys → (a : α) → Prop

• head {α : Type u} {keys : List String} {a : α} {as : Record α keys} (key : String) (not_in : ¬key ∈ keys) : Mem (Record.cons key not_in a as) a
• tail {α : Type u} {keys : List String} {a b : α} {as : Record α keys} (key : String) (not_in : ¬key ∈ keys) : Mem as a → Mem (Record.cons key not_in b as) a

instance instMembershipRecord {α : Type u} {keys : List String} : Membership α (Record α keys)

Equations

• instMembershipRecord = { mem := Mem }

inductive Contains {α : Type u} {keys : List String} : Record α keys → (key : String) → (a : α) → Type u

• head {α : Type u} {keys : List String} {a : α} {as : Record α keys} (key : String) (not_in : ¬key ∈ keys) : Contains (Record.cons key not_in a as) key a
• tail {α : Type u} {keys : List String} {a b : α} {as : Record α keys} (key' key : String) (not_in : ¬key' ∈ keys) : Contains as key a → Contains (Record.cons key' not_in b as) key a

theorem contains_to_mem {α : Type u} {key : String} {a : α} {keys : List String} {record : Record α keys} : ∀ (a✝ : Contains record key a), a ∈ record