English
For any x ∈ M F, applying dest to x and re-internalizing with M.mk yields back x: M.mk (dest x) = x.
Русский
Любой x ∈ M F удовлетворяет: M.mk (dest x) = x; переделывание через dest восстанавливает x.
LaTeX
$$$\\forall x:\\, M F,\\; M.mk(\\operatorname{dest} x) = x$$$
Lean4
@[simp]
theorem mk_dest (x : M F) : M.mk (dest x) = x := by
apply ext'
intro n
dsimp only [M.mk]
induction n with
| zero => apply @Subsingleton.elim _ CofixA.instSubsingleton
| succ n => ?_
dsimp only [Approx.sMk, dest, head]
rcases h : x.approx (succ n) with - | ⟨hd, ch⟩
have h' : hd = head' (x.approx 1) := by
rw [← head_succ' n, h, head']
apply x.consistent
revert ch
rw [h']
intro ch h
congr
ext a
dsimp only [children]
generalize hh : cast _ a = a''
rw [cast_eq_iff_heq] at hh
revert a''
rw [h]
intro _ hh
cases hh
rfl
