fact: Definition wedge_incl_comp2 : forall a, wedge_incl_elim a b0 = f_b0 a := isconn_wedge_incl.2.2.1.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc