Theorems · Theorem · logic and foundations

Computation.LiftRelAux.ret_left

∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α) (cb : Computation β),
  Computation.LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b ∈ cb, R a b

Defined in

Mathlib.Data.Seq.Computation

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound