destruct_congr — Mathlib

English

If s ~ʷ t, then the destructs of s and t are related by the lifted bisimulation: LiftRel(BisimO(· ~ʷ ·))(destruct s)(destruct t).

Русский

Если s ~ʷ t, то их деструкторы связаны через повышенное би-симуляционное отношение: LiftRel(BisimO(∼_W))(destruct s)(destruct t).

LaTeX

$$$\forall \alpha\,\forall s,t \in \mathrm{WSeq}(\alpha),\ s \sim_W t \rightarrow \mathrm{LiftRel}(\mathrm{BisimO}(\sim_W))(\mathrm{destruct}(s))(\mathrm{destruct}(t))$$$

Lean4

theorem destruct_congr {s t : WSeq α} : s ~ʷ t → Computation.LiftRel (BisimO (· ~ʷ ·)) (destruct s) (destruct t) :=
  liftRel_destruct

Похожие утверждения