theory Formula imports Nominal_Bounded_Set Nominal_Wellfounded Residual begin section ‹Infinitary Formulas› subsection ‹Infinitely branching trees› text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the powerset of trees into the set of trees), the cardinality of the argument set must be bounded.›