proposition: Theorem le_reflexive `{Funext} (x : No) : x <= x.
proof: Proof. revert x; refine (No_ind_hprop _ _); intros. apply le_lr. - intros l. refine (Conway_theorem0_lemma1 (xL l) (IHL l) _ _ _ _ 1). - intros r. refine (Conway_theorem0_lemma2 (xR r) (IHR r) _ _ _ _ 1). Defined.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core