Theorem “Initialisation for `rev`”:
      true ⇒⁅ xs := xs₀ ⨾ ys := 𝜖 ⁆ reverse xs ⌢ ys = reverse xs₀
Proof:
    reverse xs ⌢ ys = reverse xs₀
  ⁅ ys := 𝜖 ⁆⇐   ⟨ “Assignment” with substitution ⟩
    reverse xs ⌢ 𝜖 = reverse xs₀
  ⁅ xs := xs₀ ⁆⇐   ⟨ “Assignment” with substitution ⟩
    reverse xs₀ ⌢ 𝜖 = reverse xs₀
  ≡⟨“Right-identity of ⌢”⟩
    reverse xs₀ = reverse xs₀
  ≡⟨“Reflexivity of =”⟩
    true