Theorem: LO.Modal.Standard.Kripke.MultiGeachConfluent.terminal_frame (Logic/Modal/Standard/Kripke/Geach/Definability.lean)

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

State before:
case nil
α : Sort ?u.255218
inst✝ : Inhabited α
⊢ MultiGeachConfluent [] Frame.terminal.toFrame
Tactic:
simp
State after:
no goals

State before:
case cons
α : Sort ?u.255218
inst✝ : Inhabited α
t : Geach.Taple
ts : List Geach.Taple
ih : MultiGeachConfluent ts Frame.terminal.toFrame
⊢ MultiGeachConfluent (t :: ts) Frame.terminal.toFrame
Tactic:
constructor
State after:
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

State before:
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
Tactic:
. exact Kripke.GeachConfluent.terminal_frame;
State after:
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

State before:
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
Tactic:
. exact ih;
State after:
no goals

State before:
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
Tactic:
exact Kripke.GeachConfluent.terminal_frame
State after:
no goals

State before:
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
Tactic:
exact ih
State after:
no goals