proposition: Lemma pack_sigma {A} {B : A -> Type} (P : forall x : A, B x -> Type) : (forall (p : &{ x : A & B x }), P p.1 p.2) -> (forall (x : A) (y : B x), P x y).
proof: Proof. intros. apply (X &(x & y)). Defined.
imports: Equations(Equations)