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