fact: Fixpoint SimpleTypeCode_eq_semidec_transparent (T1 T2 : SimpleTypeCode) : option (T1 = T2) := match T1, T2 return option (T1 = T2) with | cnat, cnat => Some eq_refl | cbool, cbool => Some eq_refl | cstring, cstring => Some eq_refl | cascii, cascii => Some eq_refl | critem_ascii, critem_ascii => Some eq_refl | crchar_expr_ascii, crchar_expr_ascii => Some eq_refl | clist T, clist T' => match SimpleTypeCode_eq_semidec_transparent T T' with | Some p => Some (f_equal clist p) | None => None end | cprod A B, cprod A' B' => match SimpleTypeCode_eq_semidec_transparent A A', SimpleTypeCode_eq_semidec_transparent B B' with | Some p, Some q => Some (f_equal2_transparent cprod p q) | _, _ => None end | _, _ => None end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations