English
If s ~ʷ t then head s ~ head t.
Русский
Если s ~ʷ t, то голова (head) s эквивалентна голове (head) t.
LaTeX
$$$\forall s,t\in \mathrm{WSeq}(\alpha),\ s \sim_W t \rightarrow \mathrm{head}(s) \sim_W \mathrm{head}(t)$$$
Lean4
theorem head_congr : ∀ {s t : WSeq α}, s ~ʷ t → head s ~ head t :=
by
suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o => ⟨this h, this h.symm⟩
intro s t h o ho
rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩
rw [← dse]
obtain ⟨l, r⟩ := destruct_congr h
rcases l dsm with ⟨dt, dtm, dst⟩
rcases ds with - | a <;> rcases dt with - | b
· apply Computation.mem_map _ dtm
· cases b
cases dst
· cases a
cases dst
· obtain ⟨a, s'⟩ := a
obtain ⟨b, t'⟩ := b
rw [dst.left]
exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst) (some (b, t')) (destruct t) dtm
