fact: Definition syntactify_prod {A B : SimpleTypeCode} (xy : Term var A * Term var B) : Term var (A * B) := RLiteralApp Rpair (fst xy :: snd xy :: noargs).
imports: Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.Reflective.Syntax