{ 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 } }
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
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