Theorem (13.15) “Injectivity of ▹”:
    xs ▹ x = ys ▹ y  ≡  xs = ys ∧ x = y
Proof:
  By induction on `xs : Seq A`:
    Base case:
      By induction on `ys : Seq A`:
        Base case:
            𝜖 ▹ x = 𝜖 ▹ y
          ≡⟨ “Definition of ▹” ⟩
            x ◃ 𝜖 = y ◃ 𝜖
          ≡⟨ “Injectivity of ◃” ⟩
            𝜖 = 𝜖 ∧ (x = y)
        Induction step:
          For any `z`:
              𝜖 ▹ x = (z ◃ ys) ▹ y ≡ 𝜖 = z ◃ ys ∧ (x = y)
            ≡⟨ “Definition of ▹” ⟩
              x ◃ 𝜖 = z ◃ (ys ▹ y) ≡ 𝜖 = z ◃ ys ∧ (x = y)
            ≡⟨ “Injectivity of ◃” ⟩
              x = z ∧ 𝜖 = (ys ▹ y) ≡ 𝜖 = z ◃ ys ∧ (x = y)
            ≡⟨ “Snoc is not empty”, “Cons is not empty” ⟩
              x = z ∧ false ≡ false ∧ (x = y)
            ≡⟨ “Zero of ∧”, “Reflexivity of ≡” ⟩
              true
    Induction step:
      For any `w`:
        By induction on `ys : Seq A`:
          Base case:
              (w ◃ xs) ▹ x = 𝜖 ▹ y ≡ w ◃ xs = 𝜖 ∧ x = y
            ≡⟨ “Definition of ▹” ⟩
              w ◃ (xs ▹ x) = y ◃ 𝜖 ≡ w ◃ xs = 𝜖 ∧ x = y
            ≡⟨ “Injectivity of ◃” ⟩
              w = y ∧ (xs ▹ x) = 𝜖 ≡ w ◃ xs = 𝜖 ∧ x = y
            ≡⟨ “Snoc is not empty”, “Cons is not empty” ⟩
              w = y ∧ false ≡ false ∧ x = y
            ≡⟨ “Zero of ∧”, “Reflexivity of ≡” ⟩
              true
          Induction step:
            For any `z`:
                (w ◃ xs) ▹ x = (z ◃ ys) ▹ y ≡ (w ◃ xs) = (z ◃ ys) ∧ (x = y)
              ≡⟨ “Definition of ▹” ⟩
                w ◃ (xs ▹ x) = z ◃ (ys ▹ y) ≡ (w ◃ xs) = (z ◃ ys) ∧ (x = y)
              ≡⟨ “Injectivity of ◃” ⟩
                w = z ∧ (xs ▹ x) = (ys ▹ y) ≡ (w ◃ xs) = (z ◃ ys) ∧ (x = y)
              ≡⟨ Induction hypothesis `xs ▹ x = ys ▹ y  ≡  xs = ys ∧ x = y` ⟩
                (w = z ∧ xs = ys) ∧ (x = y) ≡ (w ◃ xs) = (z ◃ ys) ∧ (x = y)
              ≡⟨ “Injectivity of ◃” ⟩
                (w ◃ xs = z ◃ ys) ∧ (x = y) ≡ (w ◃ xs) = (z ◃ ys) ∧ (x = y)
              ≡⟨ “Reflexivity of ≡” ⟩
                true