fact: Fixpoint TypeCode_eq_semidec_transparent (T1 T2 : TypeCode) : option (T1 = T2) := match T1, T2 return option (T1 = T2) with | csimple T, csimple T' => option_map (f_equal csimple) (SimpleTypeCode_eq_semidec_transparent T T') | csimple _, _ => None | carrow A B, carrow A' B' => match TypeCode_eq_semidec_transparent A A', TypeCode_eq_semidec_transparent B B' with | Some p, Some q => Some (f_equal2_transparent carrow p q) | _, _ => None end | carrow _ _, _ => None end.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations