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