fact: Fixpoint Proper_relation_for (T : TypeCode) : relation (interp_TypeCode T) := match T return relation (interp_TypeCode T) with | csimple T' => eq | carrow A B => (Proper_relation_for A ==> Proper_relation_for B)%signature end.
imports: Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Common.List.ListMorphisms