Theorem: LoVe.BigStepEquiv.if_congr (LoVe/Labs/Lab6Solution.lean)

State before:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
⊢ Stmt.ifThenElse B S₁ T₁ ~ Stmt.ifThenElse B S₂ T₂
Tactic:
intro s t
State after:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t ↔ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

State before:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t ↔ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t

State before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hS₁ =>
    apply BigStep.if_true
    { assumption }
    { rw [BigStepEquiv] at hS
      rw [← hS]
      assumption }
  | if_false _ _ _ _ _ hB hT₁ =>
    apply BigStep.if_false
    { assumption }
    { rw [BigStepEquiv] at hT
      rw [← hT]
      assumption } }
State after:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t

State before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hS₂ =>
    apply BigStep.if_true
    { assumption }
    { rw [BigStepEquiv] at hS
      rw [hS]
      assumption }
  | if_false _ _ _ _ _ hB hT₂ =>
    apply BigStep.if_false
    { assumption }
    { rw [BigStepEquiv] at hT
      rw [hT]
      assumption } }
State after:
no goals

State before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
intro hif
State after:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

State before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hS₁ =>
  apply BigStep.if_true
  { assumption }
  { rw [BigStepEquiv] at hS
    rw [← hS]
    assumption }
| if_false _ _ _ _ _ hB hT₁ =>
  apply BigStep.if_false
  { assumption }
  { rw [BigStepEquiv] at hT
    rw [← hT]
    assumption }
State after:
no goals

State before:
case mp.if_true
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply BigStep.if_true
State after:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s

case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t

State before:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s

case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
{ assumption }
State after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t

State before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hS
  rw [← hS]
  assumption }
State after:
no goals

State before:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hS
State after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t

State before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
rw [← hS]
State after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₁, s) ⟹ t

State before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mp.if_false
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply BigStep.if_false
State after:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s

case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t

State before:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s

case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
{ assumption }
State after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t

State before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [← hT]
  assumption }
State after:
no goals

State before:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s
Tactic:
assumption
State after:
no goals

State before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
State after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t

State before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
rw [← hT]
State after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₁, s) ⟹ t

State before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
intro hif
State after:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t

State before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hS₂ =>
  apply BigStep.if_true
  { assumption }
  { rw [BigStepEquiv] at hS
    rw [hS]
    assumption }
| if_false _ _ _ _ _ hB hT₂ =>
  apply BigStep.if_false
  { assumption }
  { rw [BigStepEquiv] at hT
    rw [hT]
    assumption }
State after:
no goals

State before:
case mpr.if_true
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
apply BigStep.if_true
State after:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s

case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t

State before:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s

case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
{ assumption }
State after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t

State before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hS
  rw [hS]
  assumption }
State after:
no goals

State before:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s
Tactic:
assumption
State after:
no goals

State before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hS
State after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t

State before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
rw [hS]
State after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₂, s) ⟹ t

State before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mpr.if_false
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
apply BigStep.if_false
State after:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s

case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t

State before:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s

case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
{ assumption }
State after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t

State before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [hT]
  assumption }
State after:
no goals

State before:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s
Tactic:
assumption
State after:
no goals

State before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
State after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t

State before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
rw [hT]
State after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₂, s) ⟹ t

State before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
assumption
State after:
no goals