constructor <;> simp_all [symm_of_refl_eucl, trans_of_refl_eucl, eucl_of_symm_trans]
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
F✝ : Frame
⊢ MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F✝ ↔
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐊𝐓𝟒𝐁) F✝
no goals