ex3 : ∀ a b → a ≡ b → 1 + a ² ≡ b ² + 1
ex3 a b p = p
      ⇒      a  ≡ b        ⟨ (λ x → 1 + x ²) ⟩
      ⇒ 1 + a ² ≡ 1 + b ²  ⟨⟩⟨ +-comm 1 (b ²)  ⟩
      ⇒ 1 + a ² ≡ b ² + 1  ∎