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