. rfl
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ nrows t = nrows t

case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t
case a
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
hs : List ((h : Header) × Schema.HasCol h sch × Ord h.snd)
⊢ ∀ (x : (h : Header) × Schema.HasCol h sch × Ord h.snd) (a : Table sch),
    nrows a = nrows t → nrows (tsort a x.fst.fst true) = nrows t