forall a, wedge_incl_elim a b0 = f_b0 a := isconn_wedge_incl.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.