English
Alternate definition of LiftRel for relations between Computation values, by case analysis on α ⊕ Computation α.
Русский
Альтернативное определение LiftRel для отношений между значениями Computation, по случаям из суммы α ⊕ Computation α.
LaTeX
$$$\\mathrm{LiftRelAux}\\, (R\\,C) :\\alpha\\oplus\\mathrm{Computation}\\alpha \\to \\beta\\oplus\\mathrm{Computation}\\beta \\to \\mathrm{Prop}$, с определением на Sum.inl/Sum.inr: \\\\ (Sum.inl a, Sum.inl b) \mapsto R\\ a\\ b, \\\\ (Sum.inl a, Sum.inr cb) \mapsto \\exists b\\in cb\\, R\\ a b, \\\\ (Sum.inr ca, Sum.inl b) \mapsto \\exists a\\in ca\\, R\\ a b, \\\\ (Sum.inr ca, Sum.inr cb) \mapsto C\\ ca\\ cb$$$
Lean4
@[simp]
theorem liftRelAux_inl_inr {a : α} {cb} : LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b, b ∈ cb ∧ R a b :=
rfl
