Theorem: Sinf_term.succ_inj (SInfinity/Lemmas.lean)

State before:
θ₁ θ₂ : Sinf_term
⊢ θ₁↗ = θ₂↗ → θ₁ = θ₂
Tactic:
induction θ₁ <;> induction θ₂ <;> simp at *
State after:
no goals