proposition: Theorem ty_safe : forall ctx t ty ectx val, computable_valuation val -> TyRel ctx t ty -> ctxt_val val ectx ctx -> interp_term ty val ectx t.
proof: Proof. intros ctx t ty ectx val val_comp H; revert ectx val val_comp; induction H; simpl; intros; auto. - pose (P := {| comp_term := interp_term ty val; comp_val := interp_val ty val |}). assert (comp_ty : computable (interp_pair ty val)) by (unfold interp_pair; auto). destruct comp_ty. edestruct H0 as [v [lookup_v comp_v]]; eauto. simpl in *. eapply comp_term_of_val0; now eauto. - exists t, ectx; split; [now auto|intros]. apply IHTyRel; [now auto|]. intros n; destruct n; simpl. + intros ty eq; inversion eq; subst. destruct v. unfold ":::"; simpl. exists (VAbs t0 e); split; now auto. + intros ty; simpl. intros eq. edestruct H0 as [v' [lookup_v' comp_v']]; eauto. exists v'; unfold ":::"; destruct v; simpl; now auto. - simpl in *. edestruct IHTyRel1 as [t' [ectx' [eval_t comp_t]]]; eauto. assert (comp_ty1 : computable (interp_pair ty1 val)) by (unfold interp_pair; auto). assert (comp_ty2 : computable (interp_pair ty2 val)) by (unfold interp_pair; auto). destruct comp_ty1; destruct comp_ty2; simpl in *. assert (norm_u : norm ectx u) by auto. destruct norm_u as [v eval_u]. assert (comp_red_t_u : interp_term ty2 val (v ::: ectx') t') by (eapply comp_t; eauto). apply (comp_eval (interp_pair ty2 val)) with (ectx' := (v ::: ectx'))(t' := t'); unfold interp_pair; simpl; auto. intros; now eauto. - apply IHTyRel; eauto. apply ctxt_val_extend; auto. - simpl in *. apply ty_subst_extend; auto. Qed.
imports: List Arith Bool