proposition: Lemma pack_sigma_eq_inv {A} {B : A -> Type} (x y : A) (p : B x) (q : B y) (P : forall e : x = y, e [B] # p = q -> Type) : (forall e : &(x & p) = &(y & q), P (pr1_seq e) (pr2_seq e)) -> (forall (e : x = y) (e' : e [B] # p = q), P e e').
proof: Proof. intros. destruct e, e'. apply (X eq_refl). Defined.
imports: Equations(Equations)