congr 1
case hg.mk.intro.refl.refl.zero.h
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ σ (j + 1 + 1 + (i + i / 2)) = σ (j + (i + 1 + (i / 2 + 1)))
case hg.mk.intro.refl.refl.zero.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ j + 1 + 1 + (i + i / 2) = j + (i + 1 + (i / 2 + 1))