have := Schema.map_eq_List_map ▸ Schema.mem_map_of_HasName _ _ h
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')
case tl.mk.inl.cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
c nm : η
s' : Schema
h : Schema.HasName nm s'
ih :
  List.Unique (Schema.names s') →
    Table s' → Schema.names (Schema.removeName s' h) = List.filter (fun x => decide ¬x ∈ [nm]) (Schema.names s')
nm₁ : η
τ₁ : Type u_1
t : Table ((nm₁, τ₁) :: s')
heq : nm₁ = nm
hu : List.Unique (List.map Prod.fst s')
hnmem : ¬nm ∈ List.map Prod.fst s'
this : nm ∈ List.map Prod.fst s'
⊢ (nm₁, τ₁).fst :: List.map Prod.fst (Schema.removeName s' h) =
    List.filter (fun x => decide ¬x ∈ [nm]) ((nm₁, τ₁).fst :: List.map Prod.fst s')