Definition guided_by x (f : ∏ y, y ≤ x -> P y) H := ∏ y pyx, f y pyx = H y (λ z l, f z (cons (idpath z) l pyx)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.