apply tsort_spec1 (inst := x.snd.snd)
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
acc : Table sch
h : nrows acc = nrows t
⊢ nrows (tsort acc x.fst.fst true) = nrows acc
no goals