proposition: Theorem strongly_from_weakly_well_founded {X} {lt : X -> X -> Type} : weakly_well_founded lt -> strongly_well_founded lt.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Univalence