Theorem: Schema.hasNameOfFromCHeaders_eq_1 (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
τ : Type u_1
hpf : HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
cases sch with
| nil => contradiction
| cons s ss => simp [hasNameOfFromCHeaders]
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hpf : HasCol (nm, τ) []
cs : List (CertifiedHeader [])
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
contradiction
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
s : Header
ss : List Header
hpf : HasCol (nm, τ) (s :: ss)
cs : List (CertifiedHeader (s :: ss))
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
simp [hasNameOfFromCHeaders]
State after:
no goals