Module CoercionSubstitution

Set Implicit Arguments.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import Coercions.
Require Import Subtyping.
Require Import Environments.
Require Import PreliminaryLemmas.

-------------------------------------------------------------------------

Stability of typing by coercion substitution.

Lemma jco_substitution:
  forall C c T,
  jco C c T ->
  forall k d U,
  jenv C k U ->
  jco (remove_env_entry k C) d U ->
  jco (remove_env_entry k C) (subst_co d k c) T.

Proof.

induction 1; intros; simpl; eauto.

CoForall

eauto 7 using jenv_lift, jco_ty_weakening with j_term_substitution.

CoExists

eauto 7 using jenv_lift, jco_ty_weakening with j_term_substitution.

CoVar

eapply jenv_substitution; eauto.

CoMu

  constructor; eauto.
  repeat rewrite remove_lift_env.
  eapply IHjco with (k := S k).
  constructor; eauto using jenv_lift.
  simpl; apply jco_weakening.
  repeat rewrite <- remove_lift_env.
  eauto using jco_ty_weakening.
Qed.

Special cases.

Lemma jco_substitution_0:
  forall C U c T d,
  jco (C;; U) c T ->
  jco C d U ->
  jco C (subst_co d 0 c) T.

Proof.

intros. change C with (remove_env_entry 0 (C;; U)). eapply jco_substitution; eauto.
Qed.