proposition: Lemma uncurry_conj (A B C : Prop) : (A /\ B -> C) -> (A -> B -> C).
proof: Proof. intros H a b. exact (H (conj a b)). Defined.
imports: Equations.CoreTactics Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim