simp_all [serial_of_refl]
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐃) F
no goals