fact: Definition sigT_of_prod {A B : Type} (p : A * B) : {_ : A & B} := let (a, b) := p in existT (fun _ : A => B) a b.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String Relations Wellfounded Lexicographic_Product