fact: Definition pair_Show@{a m t} {A : Type@{a}} {B : Type@{a}} {AS:Show A} {BS:Show B} : Show@{_ t} (A*B) := fun p => let (a,b) := p in "("%char << show a << ","%char << show b << ")"%char.
imports: Coq.Strings.String Coq.Program.Wf Coq.PArith.BinPos Coq.ZArith.ZArith ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Programming.Injection ExtLib.Data.Char ExtLib.Data.String ExtLib.Data.Fun ExtLib.Core.RelDec