proposition: Lemma ctxt_val_extend : forall P n val ectx ctx, is_free_ctxt n ctx = false -> computable P -> ctxt_val val ectx ctx -> ctxt_val (extend val n P) ectx ctx.
proof: Proof. unfold ctxt_val. intros ? ? ? ? ? ? ? h n ty ?. edestruct h as [v [nth_v interp_v]]; eauto. exists v; split; auto. apply is_not_free_extend; auto. eapply is_free_ctx_nth_error; eauto. Qed.
imports: List Arith Bool