Theorems · Theorem · logic and foundations

Computation.LiftRelRec.lem

∀ {α : Type u} {β : Type v} {R : α → β → Prop} (C : Computation α → Computation β → Prop),
  (∀ {ca : Computation α} {cb : Computation β}, C ca cb → Computation.LiftRelAux R C ca.destruct cb.destruct) →
    ∀ (ca : Computation α) (cb : Computation β), C ca cb → ∀ a ∈ ca, Computation.LiftRel R ca cb

Defined in

Mathlib.Data.Seq.Computation

Cited by

1 results in Mathlib

Foundations

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