fact: Definition wedge_incl_comp1 : forall b, wedge_incl_elim a0 b = f_a0 b := isconn_wedge_incl.2.1.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc