proposition: Lemma curry_sig {A : Type} {P : A -> Type} {Q : forall (a : A) (b : P a), Prop} : (forall x : sigT P, Q (projT1 x) (projT2 x)) -> forall (a : A) (p : P a), Q a p.
proof: Proof. exact (fun H a p => H (existT _ a p)). Qed.
imports: Paco(paco)