α : Type u
β : Type v
γ : Type w
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match destruct (Seq.cons b s) with
    | none => (a, Seq.join S)
    | some s' => (a, Seq.join (Seq.cons s' S))) =
    (a, Seq.join (Seq.cons (b, s) S))
α : Type u
β : Type v
γ : Type w
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, Seq.join (Seq.cons (b, s) S))
dsimp [join]
no goals
α : Type u
β : Type v
γ : Type w
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ (match destruct (Seq.cons b s) with
    | none => (a, Seq.join S)
    | some s' => (a, Seq.join (Seq.cons s' S))) =
    (a, Seq.join (Seq.cons (b, s) S))
rw [destruct_cons]