. exact Kripke.GeachConfluent.terminal_frame;
case cons.left
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ GeachConfluent t Frame.terminal.toFrame

case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame
case cons.right
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent ts Frame.terminal.toFrame