fact: Definition associate_sigma_eq {A} {B : A -> Type} {C : forall x : A, B x -> Type} (P : forall (x y : &{ p : &{ x : A & B x } & C p.1 p.2 }) (e : x = y), Type) : (forall x y (e : x = y), P (associate_sigma_inv x) (associate_sigma_inv y) (associate_sigma_inv_eq x y e)) -> (forall x y (e : x = y), P x y e).
imports: Equations(Equations)