induction ts with
| nil => simp;
| cons t ts ih =>
  constructor;
  . exact Kripke.GeachConfluent.terminal_frame;
  . exact ih;
α : Sort ?u.255218
inst✝ : Inhabited α
ts : List Geach.Taple
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
no goals