proposition: Lemma eval_correct {n} Γ t (e : Expr Γ t) env v : eval n e env = Some v -> @eval_sem _ env _ e v.
proof: Proof. pose proof (fun_elim (f:=eval)) as H. specialize (H (fun n Γ t e m => forall env v, m env = Some v -> @eval_sem _ env _ e v) (fun n Γ t u f a v m => forall env v', @eval_sem _ env _ f v -> m env = Some v' -> @eval_sem _ env _ (app f a) v')). - rapply H; clear; intros. + discriminate. + noconf H; constructor. + noconf H; constructor. + noconf H; constructor. + unfold bind in H1. destruct (eval n e0 env) eqn:Heq; try discriminate. specialize (H _ _ Heq). specialize (H0 v0 _ _ H H1). apply H0. + unfold bind in H2. destruct (eval k xe env) eqn:Heq; try discriminate. unfold usingEnv in H2. specialize (H _ _ Heq). specialize (H0 v (all_cons v a) v'). econstructor; eauto. Qed.
imports: Program.Basics Program.Tactics Equations.Equations Coq.Vectors.VectorDef List Utf8