Theorem transfiniteRecursion {X:WellOrderedSet} (P : X -> Type) : LEM -> (∏ x:X, (∏ y, y<x -> P y) -> P x) -> (∏ x, P x).
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.