Theorem strongly_from_weakly_well_founded {X} {lt : X -> X -> Type} : weakly_well_founded lt -> strongly_well_founded lt. Proof. intros wwf_lt P H_P. exists (the_value lt P H_P wwf_lt). exact (the_comp lt P H_P wwf_lt). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.