proposition: Lemma constantOf_correct : forall {T} (t : Term interp_TypeCode T) v (H : constantOf t = Some v), interp_Term t = interp_constantOf v.
proof: Proof. unfold interp_Term; intros T t; induction t; repeat match goal with | [ t : RLiteralTerm _ |- _ ] => destruct t | [ t : RLiteralConstructor _ |- _ ] => destruct t | [ H : constantOf ?bv = Some ?dv, H' : forall a b c d, constantOf b = Some d -> _ |- _ ] => pose proof (fun c => H' _ bv c dv H); clear H | _ => progress simpler_args_for | _ => progress simpler end. 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