proposition: Lemma SimpleTypeCode_eq_semidec_is_dec : forall {T1 T2}, SimpleTypeCode_eq_semidec_transparent T1 T2 = None -> T1 <> T2.
proof: Proof. induction T1, T2; t_is_dec. Qed.
imports: Coq.Classes.Morphisms Coq.Strings.String Coq.Strings.Ascii Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Notations