proposition: Lemma computable_interp_term : forall ty val, computable_valuation val -> computable {| comp_term := interp_term ty val; comp_val := interp_val ty val |} .
proof: Proof. induction ty. simpl; intros val H; constructor; simpl; intros; try (destruct (H n); now eauto). - intros; constructor; simpl. + intros ectx t [t' [ectx' [eval_t _]]]. eexists; now eauto. + intros ectx t v eval_t [t' [ectx' [eval_t2 comp_t']]]. assert (v = VAbs t' ectx') by eauto; subst. auto. + intros ectx t v; destruct v as [t' ectx']; intros eval_t comp_t'. eexists; now eauto. - intros; constructor; simpl. + pose (P := norm_pred). assert (h := computable_norm : computable P). intros ectx t comp_t. assert (comp_t1 := comp_t _ h). assert (comp_ext : computable_valuation (extend val n P)) by auto. assert (comp_t2 := IHty _ comp_ext). destruct comp_t2; simpl in *. now auto. + intros ectx t v eval_t h P comp_p. assert (h0 : computable_valuation (extend val n P)) by auto. assert (comp_ext := IHty _ h0). destruct comp_ext; simpl in *. now eauto. + intros ectx t v eval_t h P comp_p. assert (h0 : computable_valuation (extend val n P)) by auto. assert (comp_ext := IHty _ h0). destruct comp_ext; simpl in *. now eauto. Qed.
imports: List Arith Bool