apply equiv_of_geach_defnability
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F ↔
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F