freudenthal@{u v | u < v} := Eval unfold freudenthal' in @freudenthal'@{u u u u u v u u u u u}.
Require Import Basics. Require Import Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations. Require Import Homotopy.Suspension. Require Import Homotopy.BlakersMassey.