fact: Definition contr_sigma_sigma (A : Type) (B : A -> Type) (C : A -> Type) (D : forall a, B a -> C a -> Type) {cac : Contr {x:A & C x} } (a : A) (c : C a) {ccd : Contr {y:B a & D a y c } } : Contr {ab : {x:A & B x} & {y:C ab.1 & D ab.1 ab.2 y} }.
imports: Basics Types