Lean4
/-- If we consider `x : F α` to, in some sense, contain values of type `α`, then
`Liftr r x y` relates `x` and `y` iff (1) `x` and `y` have the same shape and
(2) we can pair values `a` from `x` and `b` from `y` so that `r a b` holds. -/
def Liftr {α : Type u} (r : α → α → Prop) (x y : F α) : Prop :=
∃ u : F { p : α × α // r p.fst p.snd },
(fun t : { p : α × α // r p.fst p.snd } => t.val.fst) <$> u = x ∧
(fun t : { p : α × α // r p.fst p.snd } => t.val.snd) <$> u = y