English
For any X in WalkingReflexivePair, there exists a nonempty StructuredArrow from X to inclusionWalkingReflexivePair.
Русский
Для любого X из WalkingReflexivePair существует непустая структурированная стрелка из X в inclusionWalkingReflexivePair.
LaTeX
$$$\forall X:\text{WalkingReflexivePair},\; \operatorname{Nonempty}(\mathrm{StructuredArrow}(X,\ \text{inclusionWalkingReflexivePair}))$$$
Lean4
instance (X : WalkingReflexivePair) : Nonempty (StructuredArrow X inclusionWalkingReflexivePair) := by
cases X with
| zero => exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩
| one => exact ⟨StructuredArrow.mk (Y := zero) (𝟙 _)⟩
