Library TypeJudge
Require Import Types.
Section Typage.
Inductive eq_typ : env -> term -> term -> term -> Prop :=
| type_prop : ∀ e,
wf e ->
eq_typ e (Srt prop) (Srt prop) (Srt kind)
| type_var :
∀ e v t,
wf e ->
item_lift t e v ->
eq_typ e (Ref v) (Ref v) t
| type_abs :
∀ e T T' M M' U U' s1 s2,
eq_typ e T T' (Srt s1) ->
eq_typ (T :: e) U U' (Srt s2) ->
eq_typ (T :: e) M M' U ->
eq_typ e (Abs T M) (Abs T' M') (Prod T U)
| type_app :
∀ e u u' v v' V V' Ur Ur' s1 s2,
eq_typ e v v' V ->
eq_typ e V V' (Srt s1) ->
eq_typ e u u' (Prod V Ur) ->
eq_typ (V::e) Ur Ur' (Srt s2) ->
eq_typ e (App (Prod u Ur) v) (App (Prod u' Ur') v') (subst v Ur)
| type_prod :
∀ e T T' U U' s1 s2,
eq_typ e T T' (Srt s1) ->
eq_typ (T :: e) U U' (Srt s2) ->
eq_typ e (Prod T U) (Prod T' U') (Srt s2)
| type_beta : ∀ e T T' M M' N N' U U' s1 s2,
eq_typ e N N' T ->
eq_typ e T T' (Srt s1) ->
eq_typ (T::e) M M' U ->
eq_typ (T::e) U U' (Srt s2) ->
eq_typ e (App (Prod (Abs T M) U) N) (subst N' M') (subst N U)
| type_red : ∀ e M M' T T' s,
eq_typ e M M' T ->
eq_typ e T T' (Srt s) ->
eq_typ e M M' T'
| type_exp : ∀ e M M' T T' s,
eq_typ e M M' T' ->
eq_typ e T T' (Srt s) ->
eq_typ e M M' T
with wf : env -> Prop :=
wf_nil : wf nil
| wf_var : ∀ e T T' s,
eq_typ e T T' (Srt s) ->
wf (T::e).
Scheme eq_typ_mind := Minimality for eq_typ Sort Prop
with wf_mind := Minimality for wf Sort Prop.
Definition eq_red e M M' T:=
clos_refl_trans _ (fun x y => eq_typ e x y T) M M'.
Definition eq_conv e M M' T:=
clos_refl_sym_trans _ (fun x y => eq_typ e x y T) M M'.
Lemma eq_conv_refl : ∀ e t T, eq_conv e t t T.
red; auto with sets.
Qed.
Hint Resolve eq_conv_refl : coc.
Lemma eq_conv_sym :
∀ e t u T, eq_conv e t u T -> eq_conv e u t T.
red; intros; apply rst_sym; trivial.
Qed.
Lemma eq_conv_trans : ∀ e M M' M'' T,
eq_conv e M M' T ->
eq_conv e M' M'' T ->
eq_conv e M M'' T.
intros.
constructor 4 with M'; trivial.
Qed.
Lemma eq_red_conv : ∀ e M M' T, eq_red e M M' T -> eq_conv e M M' T.
unfold eq_red, eq_conv; intros; apply clos_rt_clos_rst; trivial.
Qed.
Lemma eq_conv_red : ∀ e T T' U,
eq_typ e T T' U -> eq_conv e T T' U.
Proof.
red; auto with sets.
Qed.
Lemma eq_conv_exp : ∀ e T T' U,
eq_typ e T T' U -> eq_conv e T' T U.
Proof.
red; intros; apply rst_sym; auto with sets.
Qed.
Hint Resolve eq_conv_red eq_conv_exp : coc.
Lemma type_eq_conv_gen : ∀ e M M' T T' s,
eq_conv e T T' (Srt s) ->
(eq_typ e M M' T -> eq_typ e M M' T') /\
(eq_typ e M M' T' -> eq_typ e M M' T).
induction 1; intros.
split; intros.
apply type_red with (2 := H); trivial.
apply type_exp with (2 := H); trivial.
auto.
destruct IHclos_refl_sym_trans; auto.
destruct IHclos_refl_sym_trans1.
destruct IHclos_refl_sym_trans2.
auto 10.
Qed.
Lemma type_eq_conv : ∀ e M M' T T' s,
eq_typ e M M' T -> eq_conv e T T' (Srt s) -> eq_typ e M M' T'.
intros.
elim type_eq_conv_gen with (M := M) (M' := M') (1 := H0); intros; auto.
Qed.
Lemma eq_conv_conv : ∀ (e : env) (M M' T T' : term) s,
eq_conv e M M' T -> eq_conv e T T' (Srt s) -> eq_conv e M M' T'.
induction 1; intros.
constructor 1.
apply type_eq_conv with T s; trivial.
red; apply rst_refl.
red; apply rst_sym.
apply IHclos_refl_sym_trans.
trivial.
red; apply rst_trans with y; auto.
apply IHclos_refl_sym_trans1; trivial.
apply IHclos_refl_sym_trans2; trivial.
Qed.
Lemma typ_wf : ∀ e t t' T, eq_typ e t t' T -> wf e.
Proof.
induction 1; trivial.
Qed.
Lemma typ_refl : ∀ e t t' T, eq_typ e t t' T -> eq_typ e t t T.
Proof.
induction 1; intros.
apply type_prop; trivial.
apply type_var; trivial.
apply type_abs with U s1 s2; trivial.
apply type_app with V V' s1 s2; trivial.
apply type_prod with s1; trivial.
apply type_app with T T s1 s2; trivial.
apply type_abs with U s1 s2; trivial.
apply type_red with T s; trivial.
apply type_exp with T' s; trivial.
Qed.
Lemma typ_thin :
∀ g A e t t' T,
wf (A::g) ->
eq_typ e t t' T ->
∀ n f,
ins_in_env A n e f ->
trunc n e g ->
eq_typ f (lift_rec 1 t n) (lift_rec 1 t' n) (lift_rec 1 T n).
intros g A e t t' T H H0.
elim H0 using eq_typ_mind with (P0:=fun e => ∀ n f, ins_in_env A n e f ->
trunc n e g -> wf f); simpl; intros.
constructor; eauto.
destruct (le_gt_dec n v); intros.
constructor; eauto.
apply ins_item_lift_ge with (1 := H4); trivial.
constructor; eauto.
apply ins_item_lift_lt with (1 := H4); trivial.
apply type_abs with (lift_rec 1 U' (S n)) s1 s2; eauto with coc.
rewrite distr_lift_subst.
apply type_app with (lift_rec 1 V n) (lift_rec 1 V' n) s1 s2;
eauto with coc.
apply type_prod with s1; eauto with coc.
repeat rewrite distr_lift_subst.
apply type_beta with (lift_rec 1 T' n) (lift_rec 1 U' (S n)) s1 s2;
auto with coc.
apply type_red with (lift_rec 1 T0 n) s; auto with coc.
apply type_exp with (lift_rec 1 T' n) s; auto with coc.
inversion_clear H1; inversion H2; subst g; trivial.
inversion H3; subst n; inversion H4; subst g.
trivial.
apply wf_var with (lift_rec 1 T' n0) s; auto.
Qed.
Lemma typ_thinning :
∀ A e t t' T,
wf (A::e) ->
eq_typ e t t' T ->
eq_typ (A::e) (lift 1 t) (lift 1 t') (lift 1 T).
intros.
unfold lift.
apply typ_thin with (1 := H) (2 := H0); auto with coc.
Qed.
Lemma typ_thinning_n :
∀ f t t' T n e,
wf e ->
eq_typ f t t' T ->
trunc n e f ->
eq_typ e (lift n t) (lift n t') (lift n T).
induction n; simpl; intros.
repeat rewrite lift0; inversion_clear H1; trivial.
rewrite simpl_lift.
pattern (lift (S n) t').
rewrite simpl_lift.
pattern (lift (S n) T).
rewrite simpl_lift.
inversion H1.
subst e.
apply typ_thinning; trivial.
apply IHn; auto.
inversion_clear H.
apply typ_wf with (1 := H4).
Qed.
Lemma eq_conv_lift : ∀ e T U A x,
eq_conv e T U A ->
wf (x::e) ->
eq_conv (x::e) (lift 1 T) (lift 1 U) (lift 1 A).
red; induction 1; intros; auto with sets.
apply eq_conv_red.
apply typ_thinning; trivial.
apply rst_sym; auto.
apply rst_trans with (lift 1 y).
apply IHclos_refl_sym_trans1; trivial.
apply IHclos_refl_sym_trans2; trivial.
Qed.
Lemma typ_sub :
∀ g d t e u u' U,
eq_typ e u u' U ->
∀ d' n f,
eq_typ g d d' t ->
sub_in_env d t n e f ->
trunc n f g ->
wf f ->
eq_typ f (subst_rec d u n) (subst_rec d' u' n) (subst_rec d U n).
induction 1; simpl in *; intros.
constructor; eauto.
destruct (lt_eq_lt_dec n v) as [[fvar| eq_var]| bvar].
constructor; eauto.
apply sub_item_lift_sup with (1 := H2); trivial.
subst v; rewrite sub_item_lift_eq with (1 := H2) (2 := H0).
apply typ_thinning_n with g; eauto.
constructor; eauto.
apply nth_sub_inf with (1 := H2); trivial.
assert (wf (subst_rec d T n :: f)).
apply wf_var with (subst_rec d' T' n) s1; eauto.
apply type_abs with (subst_rec d' U' (S n)) s1 s2; eauto with coc.
rewrite distr_subst.
assert (wf (subst_rec d V n :: f)).
apply wf_var with (subst_rec d' V' n) s1; eauto.
apply type_app with (subst_rec d V n) (subst_rec d' V' n) s1 s2;
eauto with coc.
assert (wf (subst_rec d T n :: f)).
apply wf_var with (subst_rec d' T' n) s1; eauto.
apply type_prod with s1; eauto with coc.
repeat rewrite distr_subst.
assert (wf (subst_rec d T n :: f)).
apply wf_var with (subst_rec d' T' n) s1; eauto.
apply type_beta with (subst_rec d' T' n) (subst_rec d' U' (S n)) s1 s2;
auto with coc.
apply type_red with (subst_rec d T n) s; eauto with coc.
apply IHeq_typ2; eauto.
apply typ_refl with (1 := H1).
apply type_exp with (subst_rec d T' n) s; eauto with coc.
apply IHeq_typ2; eauto.
apply typ_refl with (1 := H1).
Qed.
Theorem substitution :
∀ e t u u' U d d',
eq_typ (t :: (e:env)) u u' U ->
eq_typ e d d' t ->
eq_typ e (subst d u) (subst d' u') (subst d U).
Proof.
intros.
unfold subst.
apply typ_sub with (1 := H) (2 := H0); auto with coc.
apply typ_wf with (1 := H0).
Qed.
Lemma eq_conv_subst_ty_l : ∀ e M M' T U s,
eq_conv e M M' T ->
eq_typ (T::e) U U (Srt s) ->
eq_conv e (subst M U) (subst M' U) (Srt s).
red; induction 1; intros; auto with sets.
apply rst_step.
change (Srt s) with (subst x (Srt s)).
apply substitution with T; trivial.
apply rst_sym.
auto.
apply rst_trans with (subst y U); auto.
Qed.
Lemma eq_conv_subst_r : ∀ e M T U U' A,
eq_typ e M M T ->
eq_conv (T::e) U U' A ->
eq_conv e (subst M U) (subst M U') (subst M A).
red; induction 2; intros; auto with sets.
apply rst_step.
apply substitution with T; trivial.
apply rst_trans with (subst M y); auto.
Qed.
Inductive red1_in_env : env -> env -> Prop :=
| red1_env_hd : ∀ e t u s, eq_conv e t u (Srt s) ->
red1_in_env (t :: e) (u :: e)
| red1_env_tl :
∀ e f t, red1_in_env e f -> red1_in_env (t :: e) (t :: f).
Hint Constructors red1_in_env: coc.
Lemma red_item :
∀ n t e f,
item_lift t e n ->
red1_in_env e f ->
wf f ->
item_lift t f n \/
(∀ g, trunc (S n) e g -> trunc (S n) f g) /\
(exists2 u, exists s, eq_conv f t u (Srt s) & item_lift u f n).
simple induction n.
do 4 intro.
elim H.
do 3 intro.
rewrite H0.
inversion_clear H1.
intro.
inversion_clear H1; intros.
right.
split; intros.
inversion_clear H3; auto with coc.
exists (lift 1 u).
exists s.
change (Srt s) with (lift 1 (Srt s)).
apply eq_conv_lift; trivial.
exists u; auto with coc.
left.
exists x; auto with coc.
do 6 intro.
elim H0.
do 3 intro.
rewrite H1.
inversion_clear H2.
intro.
inversion_clear H2; intros.
left.
exists x; auto with coc.
elim H with (lift (S n0) x) l f0; auto with coc; intros.
left.
elim H5; intros.
exists x0; auto with coc.
rewrite simpl_lift.
pattern (lift (S (S n0)) x0).
rewrite simpl_lift.
elim H6; auto with coc.
right.
elim H5.
simple induction 2; intros.
split; intros.
inversion_clear H10; auto with coc.
elim H9; intros.
exists (lift (S (S n0)) x1).
rewrite simpl_lift.
pattern (lift (S (S n0)) x1).
rewrite simpl_lift.
destruct H8 as (s, H8).
exists s.
change (Srt s) with (lift 1 (Srt s)).
apply eq_conv_lift; trivial.
subst x0; trivial.
exists x1; auto with coc.
exists x; auto with coc.
inversion_clear H2.
apply typ_wf with (1 := H5).
Qed.
Lemma typ_red_env_raw :
∀ e t t' T, eq_typ e t t' T -> ∀ f, red1_in_env e f -> wf f ->
eq_typ f t t' T.
induction 1; intros.
apply type_prop; trivial.
elim red_item with (1 := H0) (2 := H1); auto with coc; intros.
apply type_var; auto.
destruct H3.
destruct H4; destruct H4 as (s,H4).
apply type_eq_conv with x s.
apply type_var; trivial.
red; apply rst_sym; trivial.
assert (wf (T :: f)).
apply wf_var with T' s1; auto.
apply type_abs with U' s1 s2; auto with coc.
assert (wf (V :: f)).
apply wf_var with V' s1; auto.
apply type_app with V V' s1 s2; auto with coc.
assert (wf (T :: f)).
apply wf_var with T' s1; auto.
apply type_prod with s1; auto with coc.
assert (wf (T :: f)).
apply wf_var with T' s1; auto.
apply type_beta with T' U' s1 s2; auto with coc.
apply type_red with T s; auto with coc.
apply type_exp with T' s; auto with coc.
Qed.
Lemma typ_refl2 : ∀ e M M' T, eq_typ e M M' T -> eq_typ e M' M' T.
induction 1; intros.
apply type_prop; trivial.
apply type_var; trivial.
assert (wf (T' :: e)).
apply wf_var with T' s1; trivial.
assert (red1_in_env (T :: e) (T' :: e)).
constructor 1 with s1; auto with coc.
apply type_exp with (Prod T' U) s2; auto.
apply type_abs with U' s1 s2; auto.
apply typ_red_env_raw with (T :: e); auto.
apply typ_red_env_raw with (T :: e); auto.
apply type_prod with s1; auto.
apply typ_refl with U'; trivial.
assert (wf (V' :: e)).
apply wf_var with V' s1; trivial.
assert (red1_in_env (V :: e) (V' :: e)).
constructor 1 with s1; auto with coc.
apply type_exp with (subst v' Ur') s2.
apply type_app with V V s1 s2; auto.
apply typ_refl with V'; trivial.
apply type_red with (Prod V Ur) s2; trivial.
apply type_prod with s1; trivial.
apply typ_refl with V'; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply substitution with V; trivial.
assert (wf (T' :: e)).
apply wf_var with T' s1; trivial.
assert (red1_in_env (T :: e) (T' :: e)).
constructor 1 with s1; auto with coc.
apply type_prod with s1; auto.
apply typ_red_env_raw with (T :: e); auto.
assert (wf (T' :: e)).
apply wf_var with T' s1; trivial.
assert (red1_in_env (T :: e) (T' :: e)).
constructor 1 with s1; auto with coc.
apply type_exp with (subst N' U) s2.
apply substitution with T; auto.
change (Srt s2) with (subst N (Srt s2)).
apply substitution with T; auto.
apply typ_refl with U'; trivial.
apply type_red with T s; auto.
apply type_exp with T' s; auto.
Qed.
Lemma eq_conv_inv : ∀ e T T' U,
eq_conv e T T' U ->
T = T' \/ eq_typ e T T U /\ eq_typ e T' T' U.
induction 1; intros; try firstorder subst; auto.
right.
split.
apply typ_refl with y; trivial.
apply typ_refl2 with x; trivial.
Qed.
Lemma eq_conv_inv2 : ∀ e T T' U,
eq_conv e T T' U ->
eq_typ e T T U -> eq_typ e T' T' U.
intros.
elim eq_conv_inv with (1 := H); firstorder.
subst; trivial.
Qed.
Lemma eq_red_inv : ∀ e T T' U,
eq_red e T T' U ->
T = T' \/ eq_typ e T T U /\ eq_typ e T' T' U.
intros; apply eq_conv_inv; apply eq_red_conv; trivial.
Qed.
Lemma eq_red_inv2 : ∀ e T T' U,
eq_red e T T' U ->
eq_typ e T T U -> eq_typ e T' T' U.
intros; apply eq_conv_inv2 with T; trivial; apply eq_red_conv; trivial.
Qed.
Lemma wf_red_env_trans :
∀ e f,
clos_refl_trans _ red1_in_env e f ->
wf e ->
wf f.
induction 1; auto.
induction H; intros.
elim eq_conv_inv with (1 := H); intros.
subst u; trivial.
destruct H1.
apply wf_var with u s; trivial.
inversion_clear H0.
apply wf_var with T' s.
apply typ_red_env_raw with e; trivial.
apply IHred1_in_env.
eapply typ_wf; eauto.
Qed.
Lemma typ_red_env :
∀ e f M M' T,
red1_in_env e f ->
eq_typ e M M' T ->
eq_typ f M M' T.
intros.
apply typ_red_env_raw with e; trivial.
apply wf_red_env_trans with e; auto with sets.
eapply typ_wf; eauto.
Qed.
Lemma typ_red_env_trans :
∀ e f M M' T,
clos_refl_trans _ red1_in_env e f ->
eq_typ e M M' T ->
eq_typ f M M' T.
induction 1; intros; eauto.
apply typ_red_env with x; trivial.
Qed.
Lemma eq_conv_red_env : ∀ e f x y T,
red1_in_env e f ->
eq_conv e x y T ->
eq_conv f x y T.
intros.
elim H0; intros.
red; apply rst_step.
apply typ_red_env with e; trivial.
red; apply rst_refl.
red; apply rst_sym; trivial.
red; apply rst_trans with y0; trivial.
Qed.
Lemma eq_conv_prod_r : ∀ e T U U' s1 s2,
eq_typ e T T (Srt s1) ->
eq_conv (T::e) U U' (Srt s2) ->
eq_conv e (Prod T U) (Prod T U') (Srt s2).
red; induction 2; intros; eauto with sets.
apply eq_conv_red.
apply type_prod with s1; trivial.
apply rst_trans with (Prod T y); auto.
Qed.
Lemma eq_conv_prod_l : ∀ e T T' U s1 s2,
eq_conv e T T' (Srt s1) ->
eq_typ (T::e) U U (Srt s2) ->
eq_conv e (Prod T U) (Prod T' U) (Srt s2).
red; induction 1; intros; auto with sets.
apply eq_conv_red.
apply type_prod with s1; trivial.
apply eq_conv_sym.
apply IHclos_refl_sym_trans.
apply typ_red_env with (y :: e); trivial.
constructor 1 with s1; apply eq_conv_sym; trivial.
apply eq_conv_trans with (Prod y U); red; auto.
apply IHclos_refl_sym_trans2.
apply typ_red_env with (x :: e); trivial.
constructor 1 with s1; trivial.
Qed.
Lemma eq_conv_prod : ∀ e T T' U U' s1 s2,
eq_typ e T T (Srt s1) ->
eq_typ (T::e) U U (Srt s2) ->
eq_conv e T T' (Srt s1) ->
eq_conv (T :: e) U U' (Srt s2) ->
eq_conv e (Prod T U) (Prod T' U') (Srt s2).
intros.
red; apply rst_trans with (Prod T U').
apply eq_conv_prod_r with s1; trivial.
apply eq_conv_prod_l with s1; trivial.
elim eq_conv_inv with (1 := H2); intros.
subst U'; trivial.
destruct H3; trivial.
Qed.
Lemma eq_conv_abs_r : ∀ e T M M' U s1 s2,
eq_typ e T T (Srt s1) ->
eq_typ (T::e) U U (Srt s2) ->
eq_conv (T::e) M M' U ->
eq_conv e (Abs T M) (Abs T M') (Prod T U).
red; induction 3; intros; eauto with sets.
apply rst_step.
apply type_abs with U s1 s2; trivial.
apply rst_trans with (Abs T y); trivial.
Qed.
Lemma eq_conv_abs_l : ∀ e T T' M U s1 s2,
eq_conv e T T' (Srt s1) ->
eq_typ (T::e) U U (Srt s2) ->
eq_typ (T::e) M M U ->
eq_conv e (Abs T M) (Abs T' M) (Prod T U).
red; induction 1; intros; auto with sets.
apply rst_step.
apply type_abs with U s1 s2; trivial.
apply rst_sym.
apply eq_conv_conv with (Prod x U) s2.
apply IHclos_refl_sym_trans.
apply typ_red_env with (y :: e); trivial.
constructor 1 with s1; apply eq_conv_sym; trivial.
apply typ_red_env with (y :: e); trivial.
constructor 1 with s1; apply eq_conv_sym; trivial.
apply eq_conv_prod_l with s1; trivial.
apply typ_red_env with (y :: e); trivial.
constructor 1 with s1; apply eq_conv_sym; trivial.
apply rst_trans with (Abs y M); auto.
apply eq_conv_conv with (Prod y U) s2.
apply IHclos_refl_sym_trans2.
apply typ_red_env with (x :: e); trivial.
constructor 1 with s1; trivial.
apply typ_red_env with (x :: e); trivial.
constructor 1 with s1; trivial.
apply eq_conv_sym; trivial.
apply eq_conv_prod_l with s1; trivial.
Qed.
Lemma eq_conv_abs : ∀ e T T' M M' U s1 s2,
eq_typ e T T (Srt s1) ->
eq_typ (T::e) U U (Srt s2) ->
eq_typ (T::e) M M U ->
eq_conv e T T' (Srt s1) ->
eq_conv (T::e) M M' U ->
eq_conv e (Abs T M) (Abs T' M') (Prod T U).
intros.
red; apply rst_trans with (Abs T M').
apply eq_conv_abs_r with s1 s2; trivial.
apply eq_conv_abs_l with s1 s2; trivial.
apply eq_conv_inv2 with M; trivial.
Qed.
Lemma eq_conv_app_r : ∀ e u v v' Ur V s1 s2,
eq_typ e V V (Srt s1) ->
eq_typ e u u (Prod V Ur) ->
eq_typ (V::e) Ur Ur (Srt s2) ->
eq_conv e v v' V ->
eq_typ e v v V ->
eq_conv e (App (Prod u Ur) v) (App (Prod u Ur) v') (subst v Ur).
red; induction 4; intros; eauto with sets.
apply rst_step.
apply type_app with V V s1 s2; trivial.
apply rst_sym.
apply eq_conv_conv with (subst x Ur) s2.
apply IHclos_refl_sym_trans; trivial.
apply eq_conv_inv2 with y; trivial.
apply eq_conv_sym; trivial.
apply eq_conv_subst_ty_l with V; trivial.
apply rst_trans with (App (Prod u Ur) y); auto.
apply eq_conv_conv with (subst y Ur) s2.
apply IHclos_refl_sym_trans2; trivial.
apply eq_conv_inv2 with x; trivial.
apply eq_conv_sym.
apply eq_conv_subst_ty_l with V; trivial.
Qed.
Lemma eq_conv_app_m : ∀ e u v T Ur Ur' s1 s2,
eq_typ e v v T ->
eq_typ e T T (Srt s1) ->
eq_conv (T::e) Ur Ur' (Srt s2) ->
eq_typ e u u (Prod T Ur) ->
eq_typ (T::e) Ur Ur (Srt s2) ->
eq_conv e (App (Prod u Ur) v) (App (Prod u Ur') v) (subst v Ur).
red; induction 3; intros; auto with sets.
apply rst_step.
apply type_app with T T s1 s2; trivial.
apply rst_sym.
apply eq_conv_conv with (subst v x) s2.
apply IHclos_refl_sym_trans; trivial.
apply type_eq_conv with (Prod T y) s2; trivial.
apply eq_conv_prod_r with s1; trivial.
apply eq_conv_sym; trivial.
apply eq_conv_inv2 with y; trivial.
apply eq_conv_sym; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply eq_conv_subst_r with T; trivial.
apply rst_trans with (App (Prod u y) v); auto.
apply eq_conv_conv with (subst v y) s2.
apply IHclos_refl_sym_trans2; trivial.
apply type_eq_conv with (Prod T x) s2; trivial.
apply eq_conv_prod_r with s1; trivial.
apply eq_conv_inv2 with x; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply eq_conv_subst_r with T; trivial.
apply eq_conv_sym; trivial.
Qed.
Lemma eq_conv_app_l : ∀ e u u' v T Ur s1 s2,
eq_typ e v v T ->
eq_typ e T T (Srt s1) ->
eq_typ (T::e) Ur Ur (Srt s2) ->
eq_conv e u u' (Prod T Ur) ->
eq_conv e (App (Prod u Ur) v) (App (Prod u' Ur) v) (subst v Ur).
red; induction 4; intros; auto with sets.
apply rst_step.
apply type_app with T T s1 s2; trivial.
apply rst_trans with (App (Prod y Ur) v); auto.
Qed.
Lemma eq_conv_app : ∀ e u u' v v' Ur Ur' V s1 s2,
eq_typ e v v V ->
eq_typ e V V (Srt s1) ->
eq_typ e u u (Prod V Ur) ->
eq_typ (V::e) Ur Ur (Srt s2) ->
eq_conv e u u' (Prod V Ur) ->
eq_conv e v v' V ->
eq_conv (V :: e) Ur Ur' (Srt s2) ->
eq_conv e (App (Prod u Ur) v) (App (Prod u' Ur') v') (subst v Ur).
intros.
red; apply rst_trans with (App (Prod u' Ur) v).
apply eq_conv_app_l with V s1 s2; trivial.
apply rst_trans with (App (Prod u' Ur') v).
apply eq_conv_app_m with V s1 s2; trivial.
apply eq_conv_inv2 with u; trivial.
apply eq_conv_conv with (subst v Ur') s2.
apply eq_conv_app_r with V s1 s2; trivial.
apply type_eq_conv with (Prod V Ur) s2.
apply eq_conv_inv2 with u; trivial.
apply eq_conv_prod_r with s1; trivial.
apply eq_conv_inv2 with Ur; trivial.
apply eq_conv_sym.
change (Srt s2) with (subst v (Srt s2)).
apply eq_conv_subst_r with V; trivial.
Qed.
Section Equivalence1.
Fixpoint unmark_app (t:term) : term :=
match t with
| App (Prod u _) v => App (unmark_app u) (unmark_app v)
| Abs T M => Abs (unmark_app T) (unmark_app M)
| Prod T U => Prod (unmark_app T) (unmark_app U)
| _ => t
end.
Definition unmark_env (e:env) : env := map unmark_app e.
Lemma unmark_env_cons_inv : ∀ e1 T e,
unmark_env e1 = T :: e ->
exists2 T', unmark_app T' = T &
exists2 e', unmark_env e' = e & e1 = T' :: e'.
intros.
destruct e1; try discriminate.
unfold unmark_env in *.
simpl in H.
injection H; intros.
exists t; trivial.
exists e1; trivial.
Qed.
Lemma unmark_sort_inv : ∀ T s, unmark_app T = Srt s -> T = Srt s.
destruct T; try (intros; discriminate).
auto.
destruct T1; intros; discriminate.
Qed.
Lemma unmark_prod_inv : ∀ T A B,
unmark_app T = Prod A B ->
exists2 A', unmark_app A' = A &
exists2 B', unmark_app B' = B & T = Prod A' B'.
destruct T; try (intros; discriminate).
destruct T1; intros; discriminate.
simpl; intros.
injection H; intros.
exists T1; trivial.
exists T2; trivial.
Qed.
Lemma unmark_lift : ∀ n t k,
unmark_app (lift_rec n t k) = lift_rec n (unmark_app t) k.
induction t; simpl; intros; trivial.
destruct (le_gt_dec k n0); simpl; trivial.
rewrite IHt1; rewrite IHt2; reflexivity.
destruct t1; simpl in *; auto.
destruct (le_gt_dec k n0); trivial.
assert (H := IHt1 k); clear IHt1.
injection H; intros.
rewrite IHt2; rewrite H1; reflexivity.
rewrite IHt1; rewrite IHt2; reflexivity.
Qed.
Lemma unmark_item_lift : ∀ t e n,
item_lift t e n -> item_lift (unmark_app t) (unmark_env e) n.
destruct 1; intros.
subst t.
unfold lift.
rewrite unmark_lift.
exists (unmark_app x); trivial.
unfold unmark_env.
elim H0; simpl; intros; auto with coc.
Qed.
Lemma unmark_env_item : ∀ e e' n t,
unmark_env e' = e ->
item_lift t e n ->
exists2 t', unmark_app t' = t & item_lift t' e' n.
destruct 2; intros.
subst t.
generalize e' H; clear e' H.
induction H1; intros.
destruct e'; try discriminate.
injection H; intros.
exists (lift 1 t).
unfold lift; rewrite unmark_lift.
rewrite H1; trivial.
exists t; auto.
destruct e'; try discriminate.
injection H; intros.
elim (IHitem _ H0); intros.
exists (lift 1 x0).
unfold lift; rewrite unmark_lift; rewrite H3.
change (lift 1 (lift (S n) x) = lift (S (S n)) x).
rewrite <- simpl_lift.
trivial.
unfold lift; apply ins_item_lift_ge with t e'; auto with coc arith.
Qed.
Lemma unmark_subst : ∀ N e M M' T,
eq_typ e M M' T ->
∀ k,
unmark_app (subst_rec N M k) = subst_rec (unmark_app N) (unmark_app M) k.
induction 1; simpl; intros; auto.
destruct (lt_eq_lt_dec k v) as [[_| _]| _]; trivial.
unfold lift; apply unmark_lift.
rewrite IHeq_typ1; rewrite IHeq_typ3; trivial.
rewrite IHeq_typ1; rewrite IHeq_typ3; trivial.
rewrite IHeq_typ1; rewrite IHeq_typ2; trivial.
rewrite IHeq_typ1; rewrite IHeq_typ2; rewrite IHeq_typ3; trivial.
Qed.
Lemma unmark_subst0 : ∀ N e M M' T,
eq_typ e M M' T ->
unmark_app (subst N M) = subst (unmark_app N) (unmark_app M).
Proof (fun N e M M' T H => unmark_subst N e M M' T H 0).
Lemma unmark_subst2 : ∀ N e M M' T,
eq_typ e M M' T ->
∀ k,
unmark_app (subst_rec N M' k) = subst_rec (unmark_app N) (unmark_app M') k.
intros.
apply unmark_subst with e M' T.
apply typ_refl2 with M; trivial.
Qed.
Lemma eq_typ_par_red0 : ∀ e M M' T,
eq_typ e M M' T -> par_red1 (unmark_app M) (unmark_app M').
induction 1; intros; simpl; auto with coc.
unfold subst.
rewrite unmark_subst2 with (1 := H1).
fold (subst (unmark_app N') (unmark_app M')).
auto with coc.
Qed.
Lemma eq_typ_typ : ∀ e M M' T,
eq_typ e M M' T ->
typ (unmark_env e) (unmark_app M) (unmark_app T).
intros.
elim H using eq_typ_mind with (P0 := fun e => Types.wf (unmark_env e));
simpl; intros; auto with coc.
constructor; trivial.
constructor; trivial.
apply unmark_item_lift; trivial.
apply Types.type_abs with s1 s2; trivial.
rewrite unmark_subst0 with (1 := H6).
apply Types.type_app with (unmark_app V); simpl; trivial.
apply Types.type_prod with s1; trivial.
rewrite unmark_subst0 with (1 := H6).
apply Types.type_app with (unmark_app T0); trivial.
apply Types.type_abs with s1 s2; trivial.
apply type_conv with (unmark_app T0) s; trivial.
apply red_conv.
apply par_red_red.
constructor 1.
apply eq_typ_par_red0 with (1 := H2).
apply subject_reduction with (unmark_app T0); trivial.
apply par_red_red.
constructor 1.
apply eq_typ_par_red0 with (1 := H2).
apply type_conv with (unmark_app T') s; trivial.
apply sym_conv.
apply red_conv.
apply par_red_red.
constructor 1.
apply eq_typ_par_red0 with (1 := H2).
constructor.
unfold unmark_env; simpl.
apply Types.wf_var with s; trivial.
Qed.
End Equivalence1.
Section CC_Is_Functional.
Lemma sort_uniqueness : ∀ e M M1 M2 s1 s2,
eq_typ e M M1 (Srt s1) ->
eq_typ e M M2 (Srt s2) ->
s1 = s2.
intros.
apply conv_sort.
apply typ_unique with (unmark_env e) (unmark_app M); eauto.
change (Srt s1) with (unmark_app (Srt s1)).
apply eq_typ_typ with M1; trivial.
change (Srt s2) with (unmark_app (Srt s2)).
apply eq_typ_typ with M2; trivial.
Qed.
Lemma eq_conv_sort_trans : ∀ e T U V s1 s2,
eq_conv e T U (Srt s1) ->
eq_conv e U V (Srt s2) ->
eq_typ e T T (Srt s1) ->
eq_conv e T V (Srt s1).
intros.
elim eq_conv_inv with (1 := H0); intros.
subst V; trivial.
destruct H2.
apply eq_conv_trans with U; trivial.
rewrite sort_uniqueness with e U U U s1 s2; trivial.
apply eq_conv_inv2 with T; trivial.
Qed.
Lemma wf_sort_lift :
∀ n e t, wf e -> item_lift t e n ->
exists s, eq_typ e t t (Srt s).
simple induction n.
simple destruct e; intros.
elim H0; intros.
inversion_clear H2.
elim H0; intros.
rewrite H1.
inversion_clear H2.
inversion_clear H.
exists s.
change (Srt s) with (lift 1 (Srt s)).
apply typ_thinning; auto with coc.
apply wf_var with T' s; auto with coc.
apply typ_refl with (1 := H2).
intros.
elim H1; intros.
rewrite H2.
generalize H0.
inversion_clear H3; intros.
rewrite simpl_lift; auto with coc.
cut (wf l); intros.
elim H with l (lift (S n0) x); intros; trivial.
exists x0.
change (Srt x0) with (lift 1 (Srt x0)).
apply typ_thinning; auto with coc.
exists x; auto with coc.
inversion_clear H3.
apply typ_wf with (1 := H5).
Qed.
Theorem type_case :
∀ e t t' T, eq_typ e t t' T ->
exists s, T = Srt s \/ eq_typ e T T (Srt s).
simple induction 1; intros; auto with coc.
exists kind; auto.
elim wf_sort_lift with (2 := H1); trivial; intros.
exists x; auto.
exists s2; right.
apply typ_refl with (Prod T' U').
apply type_prod with s1; auto with coc.
exists s2; right.
apply typ_refl with (subst v' Ur').
change (Srt s2) with (subst v (Srt s2)).
apply substitution with V; trivial.
exists s2;auto.
exists s2; right.
apply typ_refl with (subst N' U').
change (Srt s2) with (subst N (Srt s2)).
apply substitution with T0; trivial.
exists s;right.
apply typ_refl2 with (1 := H2).
exists s;right.
apply typ_refl with (1 := H2).
Qed.
Definition inv_type (P : Prop) e t t' T :=
match t with
| Srt s1 => ∀ s,
s1 = prop -> eq_conv e (Srt kind) T (Srt s) -> t' = (Srt s1) -> P
| Ref n =>
∀ x s, item_lift x e n -> eq_conv e x T (Srt s) -> t' = Ref n -> P
| Abs A M =>
∀ A' M' U U' s1 s2,
eq_typ e A A' (Srt s1) ->
eq_typ (A :: e) M M' U ->
eq_typ (A :: e) U U' (Srt s2) ->
eq_conv e (Prod A U) T (Srt s2) -> t' = Abs A' M' -> P
| App (Prod u Ur) v =>
∀ u' v' Ur' V V' M M' U s1 s2,
eq_typ e v v' V ->
eq_typ e V V' (Srt s1) ->
eq_typ e u u' (Prod V Ur) ->
eq_typ (V::e) Ur Ur' (Srt s2) ->
eq_typ (V::e) M M' U ->
t' = App (Prod u' Ur') v' \/
u=Abs V M /\ U = Ur /\ t' = subst v' M' ->
eq_conv e (subst v Ur) T (Srt s2) -> P
| Prod A B =>
∀ A' B' s1 s2 s,
eq_typ e A A' (Srt s1) ->
eq_typ (A :: e) B B' (Srt s2) ->
eq_conv e (Srt s2) T (Srt s) -> t' = Prod A' B' -> P
| _ => True
end.
Lemma inv_type_conv :
∀ P e t t' U V s, eq_conv e U V (Srt s) ->
inv_type P e t t' V -> inv_type P e t t' U.
do 8 intro.
elim eq_conv_inv with (1 := H); intros.
subst U; trivial.
destruct H0.
destruct t; simpl in H1 |- *; intros.
apply H1 with s; trivial.
apply eq_conv_sym; apply eq_conv_sort_trans with U s1;
try apply eq_conv_sym; trivial.
apply H1 with x s; trivial.
apply eq_conv_sym; apply eq_conv_sort_trans with U s0;
try apply eq_conv_sym; trivial.
apply H1 with A' M' U0 U' s1 s2; trivial.
apply eq_conv_sort_trans with U s; trivial.
apply type_prod with s1; trivial.
apply typ_refl with A'; trivial.
apply typ_refl with U'; trivial.
destruct t1; intros; trivial.
apply H1 with u' v' Ur' V0 V' M M' U0 s1 s2; trivial.
apply eq_conv_sort_trans with U s; trivial.
change (Srt s2) with (subst t2 (Srt s2)).
apply typ_refl with (subst v' Ur').
apply substitution with V0; trivial.
apply H1 with A' B' s1 s2 s; trivial.
apply eq_conv_sym; apply eq_conv_sort_trans with U s0; trivial;
apply eq_conv_sym; trivial.
Qed.
Theorem typ_inversion :
∀ P e t t' T, eq_typ e t t' T -> inv_type P e t t' T -> P.
induction 1; simpl; intros; eauto with coc sets.
apply H3 with (Abs T' M') N' U' T T' M M' U s1 s2; auto with coc sets.
apply type_abs with U' s1 s2; trivial.
apply IHeq_typ1.
apply inv_type_conv with T' s; auto with coc.
apply IHeq_typ1.
apply inv_type_conv with T s; auto with coc.
Existential 1 := prop.
Existential 1 := prop.
Existential 1 := prop.
Qed.
Lemma eq_typ_not_kind : ∀ e M M' T,
eq_typ e M M' T ->
M <> Srt kind.
Proof.
red; intros; subst M.
apply typ_inversion with (1 := H); red; simpl; intros; trivial.
discriminate.
Qed.
Lemma red_prod_prod_eq : ∀ e T U K,
eq_red e T U K ->
∀ A B, T = Prod A B ->
∀ (P:Prop),
(∀ A' B' s1 s2, U = Prod A' B' ->
eq_conv e A A' (Srt s1) -> eq_conv (A::e) B B' (Srt s2) -> P) -> P.
induction 1; intros; eauto with coc sets.
subst x.
apply typ_inversion with (1 := H); red; intros.
eauto with coc.
elim eq_red_inv with (1 := H); intros.
subst y; eapply IHclos_refl_trans2; eauto.
apply IHclos_refl_trans1 with (1 := H1); intros.
apply IHclos_refl_trans2 with (1 := H4); intros.
destruct H3.
rewrite H1 in H3.
apply typ_inversion with (1 := H3); simpl; intros.
apply H2 with A'0 B'0 s4 s5; trivial.
apply eq_conv_sort_trans with A' s0; trivial.
apply eq_conv_sort_trans with A s1; auto with coc.
apply typ_refl with A'1; trivial.
apply typ_refl with A'1; trivial.
apply eq_conv_sort_trans with B' s3; auto with coc.
apply eq_conv_sort_trans with B s2; auto with coc.
apply typ_refl with B'1; trivial.
apply eq_conv_red_env with (A' :: e); trivial.
constructor 1 with s1.
apply eq_conv_sym; trivial.
apply typ_refl with B'1; trivial.
Existential 1:=prop.
Existential 1:=prop.
Qed.
Lemma red_prod_prod : ∀ e A B U K,
eq_red e (Prod A B) U K ->
∀ (P:Prop),
(∀ A' B' s1 s2, U = Prod A' B' -> eq_conv e A A' (Srt s1) ->
eq_conv (A::e) B B' (Srt s2) -> P) -> P.
intros.
apply red_prod_prod_eq with e (Prod A B) U K A B; eauto.
Qed.
Lemma eq_typ_uniqueness :
∀ e M M' T',
eq_typ e M M' T' ->
∀ M'' T'',
eq_typ e M M'' T'' ->
exists s, eq_conv e T' T'' (Srt s).
induction 1; intros.
apply typ_inversion with (1 := H0); simpl; intros.
exists s; trivial.
apply typ_inversion with (1 := H1); simpl; intros.
rewrite item_lift_fun with (1 := H0) (2 := H2).
exists s; trivial.
apply typ_inversion with (1 := H2); simpl; intros.
exists s3.
assert (s1 = s0).
apply sort_uniqueness with e T T' A'; trivial.
assert (eq_conv (T :: e) U U0 (Srt s2)).
elim IHeq_typ3 with (1 := H4); intros.
apply eq_conv_sort_trans with U x; auto with coc.
apply typ_refl with U'; trivial.
assert (s2 = s3).
apply sort_uniqueness with (T :: e) U0 U0 U'0; trivial.
apply eq_conv_inv2 with U; trivial.
apply typ_refl with U'; trivial.
subst s0 s3.
apply eq_conv_trans with (Prod T U0); trivial.
apply eq_conv_prod_r with s1; trivial.
apply typ_refl with T'; trivial.
apply typ_inversion with (1 := H3); simpl; intros.
exists s3; trivial.
apply typ_inversion with (1 := H1); simpl; intros.
exists s.
assert (s1 = s0).
apply sort_uniqueness with e T T' A'; trivial.
assert (s2 = s3).
apply sort_uniqueness with (T :: e) U U' B'; trivial.
subst s0 s3.
trivial.
apply typ_inversion with (1 := H3); simpl; intros.
exists s3; trivial.
elim IHeq_typ1 with (1 := H1); intros.
exists s.
apply eq_conv_sort_trans with T x; auto with coc.
apply typ_refl2 with T; trivial.
elim IHeq_typ1 with (1 := H1); intros.
exists s.
apply eq_conv_sort_trans with T' x; auto with coc.
apply typ_refl with T'; trivial.
Qed.
Lemma typ_change : ∀ e M N T,
eq_typ e M N T ->
∀ N' T',
eq_typ e M N' T' ->
eq_typ e M N T'.
intros.
elim eq_typ_uniqueness with (1 := H) (2 := H0); intros.
apply type_eq_conv with T x; trivial.
Qed.
Lemma str_confl : ∀ e A B T,
eq_typ e A B T ->
∀ e' A' B' T',
eq_typ e' A' B' T' ->
e = e' -> A = A' ->
exists2 C, eq_typ e B C T & eq_typ e B' C T'.
fix confl1 5.
destruct 1.
intros; subst e' A'.
apply typ_inversion with (1 := H0); red; intros.
subst B'.
exists (Srt prop); trivial.
constructor; trivial.
intros; subst e' A'.
apply typ_inversion with (1 := H1); red; intros.
subst B'.
exists (Ref v); trivial.
constructor; trivial.
intros; subst e' A'.
apply typ_inversion with (1 := H2); red; intros.
clear H2; subst B'.
elim confl1 with (1 := H) (2 := H3); intros; trivial.
elim confl1 with (1 := H1) (2 := H4); intros; trivial.
exists (Abs x x0).
apply type_exp with (Prod T' U) s2.
apply type_abs with U' s1 s2; trivial.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s1; auto with coc.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s1; auto with coc.
apply type_prod with s1; trivial.
apply typ_refl with U'; trivial.
apply type_eq_conv with (2 := H6).
apply type_exp with (Prod A' U0) s3.
apply type_abs with U'0 s0 s3; auto.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s0; auto with coc.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s0; auto with coc.
apply type_prod with s0; trivial.
apply typ_refl with U'0; trivial.
intros; subst A'; intros.
apply typ_inversion with (1 := H3); clear H3; red; intros.
destruct H9.
subst e' B'.
elim eq_typ_uniqueness with (1 := H) (2 := H3); intros s1' conv_V.
assert (eq_typ (V :: e) Ur Ur'0 (Srt s3)).
apply typ_red_env with (V0 :: e); trivial.
constructor 1 with s1'; apply eq_conv_sym; trivial.
elim confl1 with (1 := H) (2 := H3); intros; trivial.
elim confl1 with (1 := H1) (2 := H6); intros; trivial.
elim confl1 with (1 := H2) (2 := H4); trivial; intros.
exists (App (Prod x0 x1) x).
apply type_exp with (subst v' Ur') s2.
apply type_app with V V' s1 s2; trivial.
apply type_eq_conv with (Prod V Ur) s2; trivial.
apply eq_conv_prod_r with s1; auto with coc.
apply typ_refl with V'; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply substitution with V; trivial.
apply type_eq_conv with (2 := H10).
apply type_exp with (subst v'0 Ur'0) s3.
apply type_app with V0 V'0 s0 s3; trivial.
apply type_eq_conv with (Prod V0 Ur) s3; trivial.
apply eq_conv_prod_r with s0; auto with coc.
apply typ_refl with V'0; trivial.
apply typ_red_env with (V :: e); trivial.
constructor 1 with s1'; auto with coc.
change (Srt s3) with (subst v (Srt s3)).
apply substitution with V0; trivial.
destruct H9.
destruct H11.
subst U B'.
generalize H4 H9; clear H6 H9.
elim H1; intros; try discriminate; auto. clear H1 H9 H12 H14.
injection H16; clear H16; intros.
elim confl1 with (1 := H) (2 := H3); intros; trivial.
elim confl1 with (1 := H13) (2 := H8); intros; subst e0 e' T M0;
trivial.
assert (eq_conv e V V0 (Srt s1)).
elim eq_typ_uniqueness with (1 := H) (2 := H3); intros.
apply eq_conv_sort_trans with V x1; auto with coc.
apply typ_refl with V'; trivial.
exists (subst x x0).
apply type_exp with (subst v' Ur') s2.
apply type_beta with T'0 Ur' s1 s2; trivial.
apply type_red with V0 s4; trivial.
apply type_eq_conv with V s1; trivial.
apply typ_refl2 with V0.
apply typ_change with (Srt s4) V0; trivial.
apply eq_conv_inv2 with V; trivial.
apply typ_refl with V'; trivial.
apply typ_red_env with (V0 :: e).
constructor 1 with s4; auto with coc.
apply type_red with Ur s2; trivial.
elim eq_typ_uniqueness with (1 := H13) (2 := H8); intros.
apply type_eq_conv with (2 := H4); trivial.
apply typ_red_env with (V :: e); trivial.
constructor 1 with s1; trivial.
apply typ_red_env with (V0 :: e).
constructor 1 with s4; auto with coc.
apply typ_red_env with (V :: e).
constructor 1 with s1; trivial.
apply typ_refl2 with Ur; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply substitution with V; trivial.
apply type_eq_conv with (2 := H10).
apply type_exp with (subst v'0 Ur) s2.
apply substitution with V0; trivial.
change (Srt s2) with (subst v (Srt s2)).
apply substitution with V.
apply typ_refl with Ur'; trivial.
apply type_eq_conv with V0 s1; auto with coc.
apply eq_conv_sym; trivial.
intros; subst e' A'.
apply typ_inversion with (1 := H1); red; intros.
subst B'.
elim confl1 with (1 := H) (2 := H2); intros; trivial.
elim confl1 with (1 := H0) (2 := H3); intros; trivial.
exists (Prod x x0).
apply type_prod with s1; trivial.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s1; auto with coc.
apply type_eq_conv with (2 := H4).
apply type_prod with s0; trivial.
apply typ_red_env with (T :: e); trivial.
constructor 1 with s0; auto with coc.
intros; subst e' A'.
apply typ_inversion with (1 := H3); clear H3; red; intros.
destruct H8.
subst B'.
clear H7 M0 M'0 U0.
apply typ_inversion with (1 := H5); clear H5; red; intros.
subst u'.
elim confl1 with (1 := H) (2 := H3); intros; trivial.
elim confl1 with (1 := H1) (2 := H7); intros; trivial.
assert (eq_conv e V T (Srt s0)).
elim eq_typ_uniqueness with (1 := H3) (2 := H); intros.
apply eq_conv_sort_trans with V x1; auto with coc.
apply typ_refl with V'; trivial.
exists (subst x x0).
apply type_exp with (subst N' U) s2.
apply substitution with T; trivial.
change (Srt s2) with (subst N (Srt s2)).
apply substitution with T; trivial.
apply typ_refl with U'; trivial.
apply type_eq_conv with (2 := H9).
apply type_exp with (subst v' Ur') s3.
apply type_beta with A' Ur' s0 s3; trivial.
apply type_red with T s4; trivial.
apply type_eq_conv with V s0; trivial.
apply typ_refl2 with T.
apply typ_change with (Srt s4) T; trivial.
apply eq_conv_inv2 with V; trivial.
apply typ_refl with V'; trivial.
apply typ_red_env with (T :: e).
constructor 1 with s4; auto with coc.
apply type_red with U s3; trivial.
elim eq_typ_uniqueness with (1 := H7) (2 := H1); intros.
apply type_eq_conv with (2 := H16); trivial.
apply typ_red_env with (V :: e); trivial.
constructor 1 with s0; trivial.
apply typ_red_env with (T :: e).
constructor 1 with s4; auto with coc.
apply typ_red_env with (V :: e).
constructor 1 with s0; trivial.
apply typ_refl2 with U; trivial.
change (Srt s3) with (subst N (Srt s3)).
apply substitution with V; trivial.
destruct H8.
destruct H10.
clear H5.
injection H8; clear H8; intros; subst V M0 U0 B'.
elim confl1 with (1 := H) (2 := H3); intros; trivial.
elim confl1 with (1 := H1) (2 := H7); intros; trivial.
exists (subst x x0).
apply type_exp with (subst N' U) s2.
apply substitution with T; trivial.
change (Srt s2) with (subst N (Srt s2)).
apply substitution with T; trivial.
apply typ_refl with U'; trivial.
apply type_eq_conv with (2 := H9).
apply type_exp with (subst v' U) s2.
apply substitution with T; trivial.
change (Srt s2) with (subst N (Srt s2)).
apply substitution with T; trivial.
apply typ_refl with U'; trivial.
intros.
elim confl1 with (1 := H) (2 := H1); intros; trivial.
exists x; trivial.
apply type_red with T s; trivial.
intros.
elim confl1 with (1 := H) (2 := H1); intros; auto.
exists x; trivial.
apply type_exp with T' s; trivial.
Qed.
Lemma strip_lemma : ∀ e A B T,
eq_red e A B T ->
∀ B',
eq_typ e A B' T ->
exists2 C, eq_red e B' C T & eq_typ e B C T.
unfold eq_red; induction 1; intros.
elim str_confl with (1 := H) (2 := H0); trivial; intros.
exists x0; auto with sets.
exists B'; auto with sets.
elim IHclos_refl_trans1 with (1 := H1); intros.
elim IHclos_refl_trans2 with (1 := H3); intros.
exists x1; trivial.
apply rt_trans with x0; trivial.
Qed.
Lemma confluence : ∀ e A B T,
eq_red e A B T ->
∀ B',
eq_red e A B' T ->
exists2 C, eq_red e B' C T & eq_red e B C T.
induction 1; intros.
elim strip_lemma with (1 := H0) (2 := H); intros.
exists x0; unfold eq_red; auto with coc sets.
exists B'; red; auto with sets.
elim IHclos_refl_trans1 with (1 := H1); intros.
elim IHclos_refl_trans2 with (1 := H3); intros.
exists x1; trivial.
red; apply rt_trans with x0; trivial.
Qed.
Lemma church_rosser : ∀ e M M' T,
eq_conv e M M' T ->
exists2 N, eq_red e M N T & eq_red e M' N T.
induction 1; intros.
exists y; red; auto with sets.
exists x; red; auto with sets.
destruct IHclos_refl_sym_trans.
exists x0; trivial.
destruct IHclos_refl_sym_trans1.
destruct IHclos_refl_sym_trans2.
elim confluence with (1 := H2) (2 := H3); intros.
exists x2.
red; apply rt_trans with x0; trivial.
red; apply rt_trans with x1; trivial.
Qed.
Lemma inv_prod_l : ∀ e A B A' B' s3,
eq_conv e (Prod A B) (Prod A' B') (Srt s3) ->
exists s1, eq_conv e A A' (Srt s1).
intros.
elim eq_conv_inv with (1 := H); intros.
injection H0; intros; subst A'.
exists prop; auto with coc.
destruct H0.
elim church_rosser with (1 := H); intros.
apply red_prod_prod with (1 := H2); trivial; intros.
apply red_prod_prod with (1 := H3); trivial; intros.
subst x.
injection H7; clear H7; intros; subst A'1.
apply typ_inversion with (1 := H0); simpl; intros.
exists s5.
apply eq_conv_sort_trans with A'0 s0; trivial.
apply eq_conv_sort_trans with A s1; auto with coc.
apply typ_refl with A'1; trivial.
apply eq_conv_sym; trivial.
apply typ_refl with A'1; trivial.
Qed.
Lemma inv_prod_r : ∀ e A B A' B' s3,
eq_conv e (Prod A B) (Prod A' B') (Srt s3) ->
exists s2, eq_conv (A::e) B B' (Srt s2).
intros.
elim eq_conv_inv with (1 := H); intros.
injection H0; intros; subst B'.
exists prop; auto with coc.
destruct H0.
elim church_rosser with (1 := H); intros.
apply red_prod_prod with (1 := H2); trivial; intros.
apply red_prod_prod with (1 := H3); trivial; intros.
subst x.
injection H7; clear H7; intros; subst A'1 B'1.
apply typ_inversion with (1 := H0); simpl; intros.
exists s6.
apply eq_conv_sort_trans with B'0 s4.
apply eq_conv_sort_trans with B s2; auto with coc.
apply typ_refl with B'1; trivial.
apply eq_conv_red_env with (A'0 :: e).
constructor 1 with s1; apply eq_conv_sym; trivial.
apply eq_conv_red_env with (A' :: e).
constructor 1 with s0; trivial.
apply eq_conv_sym; trivial.
apply typ_refl with B'1; trivial.
Qed.
Inductive mpar_red1 : term -> term -> Prop :=
par_beta : ∀ M M' N N' T U : term,
mpar_red1 M M' ->
mpar_red1 N N' ->
mpar_red1 (App (Prod (Abs T M) U) N) (subst N' M')
| sort_par_red : ∀ s, mpar_red1 (Srt s) (Srt s)
| ref_par_red : ∀ n : nat, mpar_red1 (Ref n) (Ref n)
| abs_par_red : ∀ M M' T T' : term,
mpar_red1 M M' ->
mpar_red1 T T' -> mpar_red1 (Abs T M) (Abs T' M')
| app_par_red : ∀ M M' N N' U U' : term,
mpar_red1 M M' ->
mpar_red1 N N' ->
mpar_red1 U U' ->
mpar_red1 (App (Prod M U) N) (App (Prod M' U') N')
| prod_par_red : ∀ M M' N N' : term,
mpar_red1 M M' ->
mpar_red1 N N' -> mpar_red1 (Prod M N) (Prod M' N').
Lemma mpar_red1_refl : ∀ e t t' u, eq_typ e t t' u -> mpar_red1 t t.
induction 1; auto; try (constructor; auto).
constructor; trivial.
Qed.
Lemma subject_reduction :
∀ t u, mpar_red1 t u ->
∀ e t' T,
eq_typ e t t' T ->
eq_typ e t u T.
induction 1; intros.
apply typ_inversion with (1 := H1); red; intros.
clear H6 H7 M0 M'0 U0.
apply typ_inversion with (1 := H4); red; intros.
apply type_eq_conv with (2 := H8).
elim inv_prod_l with (1 := H10); intros.
apply type_beta with A' Ur' s1 s2; eauto.
apply type_eq_conv with V x; eauto.
apply eq_conv_sym; trivial.
apply typ_change with (Srt s0) T; trivial.
apply eq_conv_inv2 with V.
apply eq_conv_sort_trans with V x; auto with coc.
apply eq_conv_sym; trivial.
apply typ_refl with V'; trivial.
apply typ_refl with V'; trivial.
elim inv_prod_r with (1 := H10); intros.
apply type_eq_conv with (2 := H13).
eauto.
apply typ_red_env with (V :: e); eauto.
constructor 1 with x; apply eq_conv_sym; trivial.
apply typ_inversion with (1 := H); red; intros; subst t'; trivial.
apply typ_inversion with (1 := H); red; intros; subst t'; trivial.
apply typ_inversion with (1 := H1); red; intros.
apply type_eq_conv with (2 := H5).
apply type_abs with U' s1 s2; eauto.
apply typ_inversion with (1 := H2); red; intros.
apply type_eq_conv with (2 := H9).
apply type_app with V V' s1 s2; eauto.
apply typ_inversion with (1 := H1); red; intros.
apply type_eq_conv with (2 := H4).
apply type_prod with s1; eauto.
Qed.
Lemma red1_mpar_red1 : ∀ e x x' T,
eq_typ e x x' T ->
∀ y,
par_red1 (unmark_app x) y ->
exists2 y', mpar_red1 x y' & unmark_app y' = y.
induction 1; simpl; intros; eauto.
inversion_clear H0.
exists (Srt prop); auto.
constructor.
inversion_clear H1.
exists (Ref v); auto; constructor.
inversion_clear H2.
elim IHeq_typ1 with (1 := H4); intros.
elim IHeq_typ3 with (1 := H3); intros.
exists (Abs x x0).
constructor; trivial.
simpl.
rewrite H5; rewrite H7; trivial.
generalize IHeq_typ3.
inversion H3; intros.
elim IHeq_typ0 with (Abs T M'); intros.
destruct u; try discriminate.
elim IHeq_typ1 with (1 := H8); intros.
inversion H9.
exists (subst x0 M'0).
constructor; trivial.
apply typ_inversion with (1 := H1); simpl; intros.
specialize subject_reduction with (1 := H15) (2 := H19); intro.
specialize typ_refl2 with (1 := H23); intro.
unfold subst; rewrite unmark_subst with (1 := H24).
subst x.
simpl in H10; injection H10; clear H10; intros.
rewrite H10; rewrite H12; trivial.
destruct u1; discriminate.
auto with coc.
elim IHeq_typ1 with (1 := H8); intros.
elim IHeq_typ3 with (1 := H6); intros.
exists (App (Prod x0 Ur) x); simpl.
constructor; trivial.
apply mpar_red1_refl with (1 := H2).
rewrite H10; rewrite H12; trivial.
inversion_clear H1.
elim IHeq_typ1 with (1 := H2); intros.
elim IHeq_typ2 with (1 := H3); intros.
exists (Prod x x0); simpl.
constructor; trivial.
rewrite H4; rewrite H6; trivial.
inversion_clear H3.
elim IHeq_typ1 with (1 := H5); intros.
elim IHeq_typ3 with (1 := H4); intros.
exists (subst x x0).
constructor; trivial.
specialize subject_reduction with (1 := H7) (2 := H1); intro.
specialize typ_refl2 with (1 := H9); intro.
unfold subst; rewrite unmark_subst with (1 := H10).
rewrite H6; rewrite H8; trivial.
inversion_clear H4.
elim IHeq_typ1 with (1 := H5); intros.
elim IHeq_typ3 with (1 := H3); intros.
elim IHeq_typ2 with (1 := H6); intros.
exists (App (Prod (Abs x1 x0) U) x); simpl.
constructor; trivial.
constructor; trivial.
apply mpar_red1_refl with (1 := H2).
rewrite H7; rewrite H9; rewrite H11; trivial.
Qed.
Lemma unmark_sr :
∀ e U U' T M',
eq_typ e U U' T ->
red (unmark_app U) M' ->
exists2 M, unmark_app M = M' & eq_red e U M T.
induction 2; intros.
exists U; trivial.
red; trivial.
destruct IHred.
elim red1_mpar_red1 with e x x T N; intros.
exists x0; trivial.
red; apply rt_trans with x; trivial.
apply rt_step.
apply subject_reduction with x; trivial.
apply eq_red_inv2 with U; trivial.
apply typ_refl with U'; trivial.
apply eq_red_inv2 with U; trivial.
apply typ_refl with U'; trivial.
apply red1_par_red1.
rewrite H2; trivial.
Qed.
Lemma unmark_eq_conv : ∀ U V e U' V' T T',
eq_typ e U U' T ->
eq_typ e V V' T' ->
unmark_app U = unmark_app V ->
eq_conv e U V T.
intros U V e U' V' T T' ty_U.
generalize V V' T'; clear V V' T'.
induction ty_U; intros.
red; apply rst_step.
simpl in H1.
destruct V; try discriminate H1.
injection H1;clear H1;intro;subst s.
constructor; trivial.
destruct V1; discriminate.
destruct V; try discriminate.
injection H2; clear H2; intros.
subst v; constructor 2; trivial.
destruct V1; discriminate.
destruct V; try discriminate.
simpl in H0; injection H0; clear H0; intros.
apply typ_inversion with (1 := H); simpl; intros.
specialize IHty_U1 with (1 := H2) (2 := H1).
apply eq_conv_abs with s1 s2; trivial.
apply typ_refl with T'; trivial.
apply typ_refl with U'; trivial.
apply typ_refl with M'; trivial.
apply IHty_U3 with M'0 U0; trivial.
apply typ_red_env with (V1 :: e); auto.
constructor 1 with s1.
apply eq_conv_sym; trivial.
destruct V1; discriminate.
destruct V0; try discriminate.
apply typ_inversion with (1 := H); destruct V0_1; simpl; trivial;
intros.
simpl in H0; injection H0; clear H0; intros.
specialize IHty_U1 with (1 := H1) (2 := H0).
specialize IHty_U3 with (1 := H3) (2 := H8).
apply eq_conv_app with V s1 s2; trivial.
apply typ_refl with v'; trivial.
apply typ_refl with V'; trivial.
apply typ_refl with u'; trivial.
apply typ_refl with Ur'; trivial.
assert (eq_typ e V0_1_1 V0_1_1 (Prod V Ur)).
apply eq_conv_inv2 with u; trivial.
apply typ_refl with u'; trivial.
elim eq_typ_uniqueness with (1 := H9) (2 := H3); intros.
elim inv_prod_r with (1 := H10); intros.
apply eq_conv_sort_trans with Ur x0; auto with coc.
apply typ_refl with Ur'; trivial.
destruct V; try discriminate.
destruct V1; discriminate.
simpl in H0; injection H0; clear H0; intros.
apply typ_inversion with (1 := H); simpl; intros.
specialize IHty_U1 with (1 := H2) (2 := H1).
apply eq_conv_prod with s1; trivial.
apply typ_refl with T'; trivial.
apply typ_refl with U'; trivial.
apply IHty_U2 with B' (Srt s3); trivial.
apply typ_red_env with (V1 :: e); auto.
constructor 1 with s1.
apply eq_conv_sym; trivial.
destruct V; try discriminate.
apply typ_inversion with (1 := H); destruct V1; simpl; trivial;
intros.
simpl in H0.
destruct V1_1; try discriminate.
2:destruct V1_1_1; discriminate.
simpl in H0; injection H0; clear H0; intros.
apply typ_inversion with (1 := H3); clear H3 H6; simpl; intros.
specialize IHty_U1 with (1 := H1) (2 := H0).
specialize IHty_U2 with (1 := H3) (2 := H9).
clear IHty_U4.
apply eq_conv_app with T s1 s2; trivial.
apply typ_refl with N'; trivial.
apply typ_refl with T'; trivial.
apply type_abs with U' s1 s2; trivial.
apply typ_refl with T'; trivial.
apply typ_refl with M'; trivial.
apply typ_refl with U'; trivial.
apply eq_conv_abs with s1 s2; trivial.
apply typ_refl with T'; trivial.
apply typ_refl with U'; trivial.
apply typ_refl with M'; trivial.
apply IHty_U3 with M'1 U1; trivial.
apply typ_red_env with (V1_1_1 :: e); trivial.
constructor 1 with s1.
apply eq_conv_sym; trivial.
elim inv_prod_r with (1 := H11); intros.
apply eq_conv_sort_trans with U1 x.
assert (eq_typ (V1_1_1 :: e) V1_1_2 V1_1_2 U).
apply typ_red_env with (T :: e).
constructor 1 with s1; trivial.
apply eq_conv_inv2 with M.
apply IHty_U3 with M'1 U1; trivial.
apply typ_red_env with (V1_1_1 :: e); trivial.
constructor 1 with s1.
apply eq_conv_sym; trivial.
apply typ_refl with M'; trivial.
elim eq_typ_uniqueness with (1 := H14) (2 := H6); intros.
apply eq_conv_sort_trans with U x0; auto with coc.
apply eq_conv_red_env with (V1_1_1 :: e); trivial.
constructor 1 with s1.
apply eq_conv_sym; trivial.
apply typ_refl with U'; trivial.
apply eq_conv_red_env with (V1_1_1 :: e); trivial.
constructor 1 with s1.
apply eq_conv_sym; trivial.
apply typ_refl with U'; trivial.
apply eq_conv_conv with T s; eauto with coc.
apply eq_conv_conv with T' s; eauto with coc.
Qed.
Lemma red_env_unmark_conv : ∀ e f,
unmark_env e = unmark_env f ->
wf e ->
wf f ->
clos_refl_trans _ red1_in_env e f.
induction e; intros.
destruct f; try discriminate.
apply rt_refl.
destruct f; try discriminate.
unfold unmark_env in H; simpl in H; injection H; clear H; intros.
apply rt_trans with (a :: f).
elim IHe with f; trivial; intros.
apply rt_step.
constructor; trivial.
apply rt_trans with (a :: y); trivial.
inversion H0; eapply typ_wf; eauto.
inversion H1; eapply typ_wf; eauto.
apply rt_step.
inversion_clear H0.
inversion_clear H1.
constructor 1 with s.
apply unmark_eq_conv with T' T'0 (Srt s0); trivial.
apply typ_red_env_trans with e; trivial.
apply IHe; trivial.
eapply typ_wf; eauto.
eapply typ_wf; eauto.
Qed.
Lemma eq_typ_red_env_unmark : ∀ e f M M' T,
unmark_env e = unmark_env f ->
wf f ->
eq_typ e M M' T ->
eq_typ f M M' T.
intros.
apply typ_red_env_trans with e; trivial.
apply red_env_unmark_conv; trivial.
eapply typ_wf; eauto.
Qed.
Lemma unmark_conv_sort : ∀ e U U' V V' s1 s2,
eq_typ e U U' (Srt s1) ->
eq_typ e V V' (Srt s2) ->
conv (unmark_app U) (unmark_app V) ->
eq_conv e U V (Srt s1).
intros.
elim Conv.church_rosser with (1 := H1); intros.
elim unmark_sr with (1 := H) (2 := H2); intros.
elim unmark_sr with (1 := H0) (2 := H3); intros.
apply eq_conv_sort_trans with x0 s2.
apply eq_red_conv; trivial.
apply eq_conv_trans with x1.
apply eq_conv_sym.
apply unmark_eq_conv with x1 x0 (Srt s1).
apply eq_red_inv2 with V; trivial.
apply typ_refl with V'; trivial.
apply eq_red_inv2 with U; trivial.
apply typ_refl with U'; trivial.
rewrite H4; trivial.
apply eq_conv_sym; apply eq_red_conv; trivial.
apply typ_refl with U'; trivial.
Qed.
Lemma typ_eq_typ : ∀ e M T,
typ e M T ->
exists2 e', unmark_env e' = e &
exists2 M', unmark_app M' = M &
exists2 T', unmark_app T' = T &
eq_typ e' M' M' T'.
Proof.
intros e M T H.
elim H using typ_mind
with (P0 := fun e => exists2 e', unmark_env e' = e & wf e');
clear e M T H; simpl; intros.
destruct H0.
exists x; trivial.
exists (Srt prop); trivial.
exists (Srt kind); trivial.
constructor; trivial.
destruct H0.
exists x; trivial.
exists (Ref v); trivial.
elim unmark_env_item with (1 := H0) (2 := H1); intros.
exists x0; trivial.
constructor; trivial.
destruct H0 as (e', unmk_e, (A, unmk_A, (s1', unmk_s1, ty_A))).
rewrite unmark_sort_inv with (1 := unmk_s1) in ty_A; clear unmk_s1 s1'.
destruct H2 as (e1, unmk_e1, (U', unmk_U, (s2', unmk_s2, ty_U))).
rewrite unmark_sort_inv with (1 := unmk_s2) in ty_U; clear unmk_s2 s2'.
elim unmark_env_cons_inv with (1 := unmk_e1);
intros T1 unmk_T1 (e2, unmk_e2, eq_e1); clear unmk_e1; subst e1.
destruct H4 as (e3, unmk_e3, (M', unmk_M, (U2, unmk_U2, ty_M))).
elim unmark_env_cons_inv with (1 := unmk_e3);
intros T2 unmk_T2 (e4, unmk_e4, eq_e2); clear unmk_e3; subst e3.
exists e'; trivial.
exists (Abs A M'); simpl.
rewrite unmk_A; rewrite unmk_M; trivial.
exists (Prod A U2); simpl.
rewrite unmk_A; rewrite unmk_U2; trivial.
apply type_abs with U2 s1 s2; trivial.
assert (eq_typ (T2::e4) U' U' (Srt s2)).
apply eq_typ_red_env_unmark with (T1::e2); trivial.
unfold unmark_env; simpl; fold (unmark_env e2) (unmark_env e4).
rewrite unmk_T1; rewrite unmk_e2; rewrite unmk_T2; rewrite unmk_e4; trivial.
eapply typ_wf; eauto.
apply eq_typ_red_env_unmark with (T2::e4); trivial.
unfold unmark_env; simpl; fold (unmark_env e4) (unmark_env e').
rewrite unmk_T2; rewrite unmk_e4; rewrite unmk_A; rewrite unmk_e; trivial.
apply wf_var with A s1; trivial.
elim type_case with (1 := ty_M); intros.
destruct H2.
subst U2 U.
rewrite unmark_sort_inv with U' x in H0; auto with coc.
apply eq_conv_inv2 with U'; trivial.
apply unmark_eq_conv with (1 := H0) (2 := H2); trivial.
rewrite unmk_U2; auto.
apply eq_typ_red_env_unmark with (T2::e4); trivial.
unfold unmark_env; simpl; fold (unmark_env e4) (unmark_env e').
rewrite unmk_T2; rewrite unmk_e4; rewrite unmk_A; rewrite unmk_e; trivial.
apply wf_var with A s1; trivial.
destruct H0 as (e', unmk_e, (v', unmk_v, (V', unmk_V, ty_v))).
destruct H2 as (e1, unmk_e1, (u', unmk_u, (U', unmk_U, ty_u))).
exists e'; trivial.
specialize unmark_prod_inv with (1 := unmk_U).
intros (V1, eq_V, (Ur', eq_Ur, eq_U')).
exists (App (Prod u' Ur') v'); simpl.
rewrite unmk_u; rewrite unmk_v; trivial.
subst U'.
elim type_case with (1 := ty_u); intros s [eq_s|ty_pi];
try discriminate.
exists (subst v' Ur').
unfold subst.
apply typ_inversion with (1 := ty_pi); simpl; intros.
rewrite unmark_subst with (1 := H2).
rewrite unmk_v; rewrite eq_Ur; trivial.
apply typ_inversion with (1 := ty_pi); simpl; intros.
apply type_app with V1 A' s1 s2; trivial.
elim type_case with (1 := ty_v); intros.
destruct H5.
subst V' V; simpl in unmk_V.
rewrite unmark_sort_inv with V1 x; auto with coc.
apply type_eq_conv with V' x; trivial.
apply unmark_eq_conv with V' A' (Srt s1); trivial.
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e; trivial.
apply typ_wf with (1 := ty_v).
rewrite eq_V; auto with coc.
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e; trivial.
apply typ_wf with (1 := ty_v).
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e; trivial.
apply typ_wf with (1 := ty_v).
apply typ_refl with B'.
apply eq_typ_red_env_unmark with (V1 :: e1); trivial.
unfold unmark_env; simpl.
fold (unmark_env e1).
fold (unmark_env e').
rewrite unmk_e; rewrite unmk_e1; trivial.
apply wf_var with A' s1.
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e; trivial.
apply typ_wf with (1 := ty_v).
destruct H0 as (e', unmk_e, (T', unmk_T, (s1', unmk_s1, ty_T))).
exists e'; trivial.
rewrite unmark_sort_inv with (1 := unmk_s1) in ty_T.
clear unmk_s1 s1'.
destruct H2 as (e1, unmk_e1, (U', unmk_U, (s2', unmk_s2, ty_U))).
rewrite unmark_sort_inv with (1 := unmk_s2) in ty_U.
clear unmk_s2 s2'.
exists (Prod T' U'); simpl.
rewrite unmk_T; rewrite unmk_U; trivial.
exists (Srt s2); trivial.
apply type_prod with s1; trivial.
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e1.
rewrite <- unmk_e; rewrite <- unmk_T; trivial.
apply wf_var with T' s1; trivial.
destruct H0 as (e', unmk_e, (t', unmk_t, (U', unmk_U, ty_t))).
destruct H3 as (e1, unmk_e1, (V', unmk_V, (s', unmk_s, ty_V))).
exists e'; trivial.
exists t'; trivial.
exists V'; trivial.
rewrite unmark_sort_inv with (1 := unmk_s) in ty_V.
apply type_eq_conv with U' s; trivial.
assert (exists s' : _, eq_typ e' U' U' (Srt s')).
elim type_case with (1 := ty_t); intros.
destruct H0.
exists s.
subst U' U; simpl in H1.
assert (typ e (Srt x) (Srt s)).
apply Types.subject_reduction with V; trivial.
apply Conv.church_rosser in H1; destruct H1.
apply red_normal in H0.
rewrite H0; trivial.
red; red; intros.
inversion H3.
apply Types.typ_inversion with (1 := H0); simpl; intros.
destruct x; trivial; intros.
apply conv_sort in H3; subst s.
constructor; trivial.
eapply typ_wf; eauto.
exists x; trivial.
destruct H0.
apply eq_conv_sym.
apply unmark_conv_sort with V' U' x; trivial.
apply eq_typ_red_env_unmark with e1; trivial.
rewrite unmk_e; trivial.
apply typ_wf with (1 := ty_t).
rewrite unmk_U; rewrite unmk_V; auto with coc.
exists (nil:env); auto.
constructor.
destruct H0 as (e', unmk_e, (T', unmk_T, (s', unmk_s, ty_T))).
exists (T' :: e'); trivial.
unfold unmark_env; simpl.
fold (unmark_env e').
rewrite unmk_e; rewrite unmk_T; trivial.
rewrite unmark_sort_inv with (1 := unmk_s) in ty_T.
apply wf_var with T' s; trivial.
Qed.
End CC_Is_Functional.
End Typage.