proposition: Lemma is_not_free_extend : forall ty n val P, is_free n ty = false -> (forall ectx t, interp_term ty val ectx t <-> interp_term ty (extend val n P) ectx t) /\ (forall v, interp_val ty val v <-> interp_val ty (extend val n P) v) .
proof: Proof. induction ty; simpl; intros. - unfold extend; assert (eq := Nat.eqb_eq n n0). destruct (n =? n0); split; intros; try congruence; reflexivity; eauto. - rewrite orb_false_iff in *. destruct H. split; [split; intro h; destruct h as [t' [ectx' [h1 h2]]]; exists t', ectx'; split; eauto; intros v| ]. + edestruct IHty1; edestruct IHty2; eauto. rewrite<- H3. rewrite<- H2. eauto. + edestruct IHty1; edestruct IHty2; eauto. rewrite H3. rewrite H2. eauto. + intros v; destruct v. split; intros h v; edestruct IHty1; edestruct IHty2; eauto. -- rewrite<- H2. rewrite<- H3. eauto. -- rewrite H2. rewrite H3. now eauto. - assert (eq := Nat.eqb_eq n0 n). destruct (n0 =? n). assert (n0 = n) by firstorder; subst. + assert (forall P0 k, equiv_comp_pair (extend val n P0 k) (extend (extend val n P) n P0 k)). { unfold extend; intros; destruct (k =? n); simpl; apply equiv_comp_pair_refl; eauto. } split; split; intros; eapply ty_subst_ext; intros; try apply H0; try (apply equiv_comp_pair_sym; apply H0); try apply H1; eauto. + assert (forall P0 k, equiv_comp_pair (extend (extend val n0 P) n P0 k) (extend (extend val n P0) n0 P k)). { unfold extend; intros. assert (eq' := Nat.eqb_eq k n). assert (eq'' := Nat.eqb_eq k n0). destruct (k =? n); destruct (k =? n0); simpl; try apply equiv_comp_pair_refl. assert (n0 = n) by (firstorder; congruence). exfalso. assert (false = true) by (apply eq; eauto). congruence. } split; split; intros; try (eapply ty_subst_ext; intros; apply equiv_comp_pair_sym; apply H0; apply IHty; now eauto). -- eapply ty_subst_ext; intros; try apply equiv_comp_pair_sym; try apply H0. apply IHty; eauto. -- assert (interp_term ty (extend (extend val n P0) n0 P) ectx t) by (eapply ty_subst_ext; intros; try apply H0; eauto). revert H3. apply IHty; eauto. -- eapply ty_subst_ext; intros; try apply equiv_comp_pair_sym; try apply H0; eauto. apply IHty; eauto. -- assert (interp_val ty (extend (extend val n P0) n0 P) v) by (eapply ty_subst_ext; intros; try apply H0; eauto). revert H3. apply IHty; eauto. Unshelve. auto. auto. auto. auto. auto. auto. auto. auto. Qed.
imports: List Arith Bool