English
The lifted relation is reflexive when the base relation is reflexive.
Русский
Поднятое отношение рефлексивно при условии рефлексивности базового отношения.
LaTeX
$$$$ \forall {\alpha},\ \mathrm{Refl}(R) \Rightarrow \mathrm{Reflexive}(\mathrm{LiftRel}\ R). $$$$
Lean4
theorem refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (LiftRel R) := fun s =>
by
refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
rw [← h]
apply Computation.LiftRel.refl
intro a
rcases a with - | a
· simp
· cases a
simp only [LiftRelO, and_true]
apply H