fact: Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P := exist P (let (a, _, _) := X in a) (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p).
imports: Notations Ltac Datatypes Logic