proposition: Theorem lt_wf@{} : WellFounded lt.
proof: Proof. do 2 red. apply nat_rect@{Set}; intros. - constructor. intros y Hy. depelim Hy. - constructor. intros y Hy. dependent elimination Hy as [@le_S y x Hle]. apply le_eq_lt in Hle. dependent elimination Hle as [inl idpath|inr Hlt]. + assumption. + destruct H. now apply a. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded HoTT(Spaces.Nat)