quotient_kernel_factor_general@{|} := Eval unfold quotient_kernel_factor_internal in quotient_kernel_factor_internal@{ar' ar abr abr ab abr abr}.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.