proposition: Lemma ty_subst_ext : forall ty val val', (forall n, equiv_comp_pair (val n) (val' n)) -> (forall ectx t, interp_term ty val ectx t -> interp_term ty val' ectx t) /\ (forall v, interp_val ty val v -> interp_val ty val' v).
proof: Proof. induction ty; intros val val' H; split; simpl; intros; try apply H; auto. - destruct H0 as [t' [ectx' [eval_t comp_t]]]. exists t', ectx'; split; auto. intros; eapply IHty2; [now auto | apply comp_t]. eapply IHty1; intros; [apply equiv_comp_pair_sym; now auto| now auto]. - destruct v; intros; eapply IHty2; eauto. apply H0. eapply IHty1; [intros; apply equiv_comp_pair_sym; eauto| now eauto]. - eapply IHty; [intros; apply extend_equiv; eauto| now auto]. - eapply IHty; [intros; apply extend_equiv; eauto| now auto]. Qed.
imports: List Arith Bool