Cancellation of snoc

Theorem “Cancellation 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  ≡  𝜖 = 𝜖 ∧ x = y
          =⟨ “Definition of ▹ for 𝜖” ⟩
            x ◃ 𝜖 = y ◃ 𝜖  ≡  𝜖 = 𝜖 ∧ x = y
          =⟨ “Cancellation of ◃” ⟩
            𝜖 = 𝜖 ∧ x = y  ≡  𝜖 = 𝜖 ∧ x = y
          ≡⟨ “Reflexivity of ≡” ⟩
            true
        Induction step:
          For any `c`:
              𝜖 ▹ x = (c ◃ ys) ▹ y
            =⟨ “Definition of ▹ for 𝜖” ⟩
              x ◃ 𝜖 = (c ◃ ys) ▹ y
            =⟨ “Definition of ▹ for ◃” ⟩
              x ◃ 𝜖 = c ◃ (ys ▹ y)
            =⟨ “Cancellation of ◃” ⟩
              x = c ∧ 𝜖 = (ys ▹ y)
            =⟨ “Snoc is not empty” ⟩
              x = c ∧ false
            =⟨ “Zero of ∧” ⟩
              false
            =⟨ “Cons is not empty”, “Zero of ∧” ⟩
              𝜖 = (c ◃ ys) ∧ x = y
    Induction step:
      For any `d`:
        By induction on `ys : Seq A`:
          Base case:
              (d ◃ xs) ▹ x = 𝜖 ▹ y  ≡
              (d ◃ xs) = 𝜖 ∧ x = y
            =⟨ “Cons is not empty”, “Zero of ∧” ⟩
              (d ◃ xs) ▹ x = 𝜖 ▹ y  ≡  false
            =⟨ “Definition of ▹ for 𝜖”,
              “Definition of ▹ for ◃” ⟩
              d ◃ (xs ▹ x) = y ◃ 𝜖  ≡  false
            =⟨ “Cancellation of ◃” ⟩
              d = y ∧ (xs ▹ x) = 𝜖  ≡  false
            =⟨ “Snoc is not empty”, “Zero of ∧” ⟩
              false ≡ false
            =⟨ “Reflexivity of ≡” ⟩
              true
          Induction step:
            For any `a`:
                (d ◃ xs) ▹ x = (a ◃ ys) ▹ y
              =⟨ “Definition of ▹ for ◃” ⟩
                d ◃ (xs ▹ x) = a ◃ (ys ▹ y)
              =⟨ “Cancellation of ◃” ⟩
                a = d ∧ (xs ▹ x) = (ys ▹ y)
              =⟨ Induction hypothesis
                 `xs ▹ x = ys ▹ y  ≡  xs = ys ∧ x = y` ⟩
                a = d ∧ xs = ys ∧ x = y
              =⟨ “Cancellation of ◃” ⟩
                (d ◃ xs) = (a ◃ ys) ∧ x = y