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
no goals