proposition: Lemma uncurry_prod (A B C : Type) : (A * B -> C) -> (A -> B -> C).
proof: Proof. intros H a b. exact (H (a, b)). Defined.
imports: Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec Equations.Type.DepElim