proposition: Lemma reify_and_reflect_correct : forall t, (forall v r, @related t v r -> Proper_relation_for _ v (interp_Term (reify _ r))) /\ (forall a a', @Proper_relation_for t (interp_Term a) (interp_Term a') -> @related t (interp_Term a) (reflect a')).
proof: Proof. unfold interp_Term; induction t; simpler; unfold respectful; eauto. Qed.
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