induction_generalize_premise_args.lean:12:2: error: tactic failed, there are unsolved goals
state:
h₁_c₁ h₁_c₂ : com,
h₁_σ : state,
h₁_c₁' : com,
h₁_σ' : state,
h₁_a : smallstep (h₁_c₁, h₁_σ) (h₁_c₂, h₁_σ'),
h₁_ih :
  ∀ (c'₂ : com) (σ'₂ : state),
    smallstep (h₁_c₁, h₁_σ) (c'₂, σ'₂) → (h₁_c₂, h₁_σ') = (c'₂, σ'₂),
c'₂ : com,
σ'₂ : state,
h₂ : smallstep (com.seq h₁_c₁ h₁_c₂, h₁_σ) (c'₂, σ'₂)
⊢ (com.seq h₁_c₁' h₁_c₂, h₁_σ') = (c'₂, σ'₂)
