fact: Fixpoint related {T} : interp_TypeCode T -> normalized_of interp_TypeCode T -> Prop := match T return interp_TypeCode T -> normalized_of interp_TypeCode T -> Prop with | csimple T' => fun b e => b = interp_Term e | (dom --> ran)%typecode => fun f1 f2 => forall x1 x2, related x1 x2 -> related (f1 x1) (f2 x2) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Semantics Fiat.Parsers.Reflective.PartialUnfold Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Parsers.Reflective.Morphisms Fiat.Common.List.ListFacts Fiat.Common.Equality