induction hS with
| skip => exact RTC.refl
| assign =>
  apply RTC.single
  apply SmallStep.assign
| seq S T s t u hS hT ihS ihT =>
  apply RTC.trans
  { exact RTC_SmallStep_seq ihS }
  { apply RTC.head
    apply SmallStep.seq_skip
    assumption }
| if_true B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_true
    assumption }
  { assumption }
| if_false B S T s t hB hst ih =>
  apply RTC.head
  { apply SmallStep.if_false
    assumption }
  { assumption }
| while_true B S s t u hB hS hw ihS ihw =>
  apply RTC.head
  { apply SmallStep.whileDo }
  { apply RTC.head
    { apply SmallStep.if_true
      assumption }
    { apply RTC.trans
      { exact RTC_SmallStep_seq ihS }
      { apply RTC.head
        apply SmallStep.seq_skip
        assumption } } }
| while_false B S s hB =>
  apply RTC.tail
  apply RTC.single
  apply SmallStep.whileDo
  apply SmallStep.if_false
  assumption
Ss : Stmt × State
t : State
hS : Ss ⟹ t
⊢ RTC SmallStep Ss (Stmt.skip, t)
no goals