fact: Definition to {a b c} : (a + (b + (a * b)) → option c) → (a → option (b → option c)) := fun f a => Some (fun b => f (inr (inr (a, b)))).
imports: Category.Lib Category.Theory.Category Category.Instance.Sets Category.Structure.Cartesian