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