Set Implicit Arguments.
Require Import Terms.
Require Import BT.

Axiom Extensionality_Ensembles : forall A s1 s2, (forall x : A, s1 x <-> s2 x) -> s1 = s2.

Axiom fun_extensionality_dep : forall A, forall B : (A -> Type),
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

Lemma fun_extensionality : forall A B (f g : A -> B),
  (forall x, f x = g x) -> f = g.
Proof.
  intros ; apply fun_extensionality_dep.
  assumption.
Qed.



               (* Types *)

Inductive typ : Set :=
  | typvar  : nat -> typ
  | typprod : typ -> typ -> typ
  | typref  : typ -> typ
  | typlist : typ -> typ
  | typarr  : typ -> typ -> typ
.

Inductive typfree : nat -> typ -> Prop :=
  | typfvar : forall x, typfree x (typvar x)
  | typfprod1 : forall x t1 t2, typfree x t1 -> typfree x (typprod t1 t2)
  | typfprod2 : forall x t1 t2, typfree x t2 -> typfree x (typprod t1 t2)
  | typfref : forall x t, typfree x t -> typfree x (typref t)
  | typflist : forall x t, typfree x t -> typfree x (typlist t)
  | typfarr1 : forall x t1 t2, typfree x t1 -> typfree x (typarr t1 t2)
  | typfarr2 : forall x t1 t2, typfree x t2 -> typfree x (typarr t1 t2)
.

Inductive dangerv : var -> typ -> Prop :=
  | dprod1 : forall x t1 t2, dangerv x t1 -> dangerv x (typprod t1 t2)
  | dprod2 : forall x t1 t2, dangerv x t2 -> dangerv x (typprod t1 t2)
  | dref : forall x t, typfree x t -> dangerv x (typref t)
  | dlist : forall x t, dangerv x t -> dangerv x (typlist t)
  | darr1 : forall x t1 t2, typfree x t1 -> dangerv x (typarr t1 t2)
  | darr2 : forall x t1 t2, dangerv x t2 -> dangerv x (typarr t1 t2)
.

Definition abstraction := var -> Prop.

Definition abstr (a : abstraction) := forall x, a x \/ not (a x).



Lemma tfreedec : forall x t, typfree x t \/ not (typfree x t).
intros; induction t.
destruct (diff x n).
left; rewrite H; constructor.
right; intro; inversion H0; destruct H; assumption.
case IHt1; intro.
left; apply (typfprod1 t2 H).
case IHt2; intro.
left; apply (typfprod2 t1 H0).
right; intro; inversion H1.
apply (H H4).
apply (H0 H4).
case IHt; intro.
left; constructor; assumption.
right; intro; inversion H0; apply H; assumption.
case IHt; intro.
left; constructor; assumption.
right; intro; inversion H0; apply H; assumption.
case IHt1; intro.
left; apply (typfarr1 t2 H).
case IHt2; intro.
left; apply (typfarr2 t1 H0).
right; intro; inversion H1.
apply (H H4).
apply (H0 H4).
Qed.

Hint Constructors typfree.
Lemma dangfree : forall x t, dangerv x t -> typfree x t.
intros; induction H; auto.
Qed.



               (* Ordre *)

Definition substitution := var -> typ.

Fixpoint trans (s : substitution) (t : typ) : typ :=
  match t with
  | typvar x => s x
  | typprod t1 t2 => typprod (trans s t1) (trans s t2)
  | typref t0 => typref (trans s t0)
  | typlist t0 => typlist (trans s t0)
  | typarr t1 t2 => typarr (trans s t1) (trans s t2)
  end.

Definition order t0 a t := exists s, (forall x, not (a x) -> s x = (typvar x)) /\ trans s t = t0.



               (* Environements *)

Definition benv := list (prod var (prod typ abstraction)).
Definition renv := list typ.

Inductive bound : var -> benv -> Prop :=
  | bbh : forall x t a gb, bound x (cons (x,(t,a)) gb)
  | bbt : forall x y t a gb, bound x gb -> bound x (cons (y,(t,a)) gb)
.

Inductive bcorr : benv -> Prop :=
  | bcemp : bcorr nil
  | bctyp : forall x t a gb, not (bound x gb) -> abstr a -> bcorr gb -> bcorr (cons (x,(t,a)) gb)
.

Inductive benveq : benv -> benv -> Prop :=
  | beqrefl : forall gb, benveq gb gb
  | beqcom : forall u v gb, benveq (cons u (cons v gb)) (cons v (cons u gb))
  | beqcon : forall u gb1 gb2, benveq gb1 gb2 -> benveq (cons u gb1) (cons u gb2)
  | beqtran : forall gb1 gb2 gb3, benveq gb1 gb2 -> benveq gb2 gb3 -> benveq gb1 gb3
.

Inductive benvread : var -> typ -> abstraction -> benv -> Prop :=
  | tbreadh : forall x t a gb, benvread x t a (cons (x,(t,a)) gb)
  | tbreadt : forall x t a u gb, benvread x t a gb -> benvread x t a (cons u gb)
.

Inductive benvfree : var -> benv -> Prop :=
  | bfh : forall x y t a gb, typfree x t -> benvfree x (cons (y,(t,a)) gb)
  | bft : forall x u gb, benvfree x gb -> benvfree x (cons u gb)
.

Inductive renvfree : var -> renv -> Prop :=
  | rfh : forall x t gr, typfree x t -> renvfree x (cons t gr)
  | rft : forall x t gr, renvfree x gr -> renvfree x (cons t gr)
.



Lemma readcor : forall x t a gb, bcorr gb -> benvread x t a gb -> abstr a.
intros; induction H0.
inversion H; assumption.
inversion H; apply IHbenvread; assumption.
Qed.



               (* Typage *)

Inductive typing_ax : constants -> typ -> Prop :=
  | Ytyp : forall t1 t2, typing_ax cY
             (typarr (typarr (typarr t1 t2) (typarr t1 t2)) (typarr t1 t2))
  | reftyp : forall t, typing_ax cref (typarr t (typref t))
  | exptyp : forall t, typing_ax cexp (typarr (typref t) t)
  | settyp : forall t, typing_ax cset (typarr (typprod (typref t) t) t)
  | pr1typ : forall t1 t2, typing_ax cpr1 (typarr (typprod t1 t2) t1)
  | pr2typ : forall t1 t2, typing_ax cpr2 (typarr (typprod t1 t2) t2)
  | niltyp : forall t, typing_ax cnil (typlist t)
  | ucontyp : forall t1 t2, typing_ax cucon
                (typarr (typprod (typprod (typarr (typlist t1) t2)
                                    (typarr (typprod t1 (typlist t1)) t2)) (typlist t1)) t2)
.

Inductive typing_base : term -> typ -> benv -> renv -> Prop :=
  | axtyp : forall c t gb gr, bcorr gb -> typing_ax c t -> typing_base (tcons c) t gb gr
  | fvartyp : forall x a t t0 gb gr,
                bcorr gb -> benvread x t a gb -> order t0 a t
                -> typing_base (tfvar x) t0 gb gr
  | rvartyp : forall n t gb gr,
                bcorr gb -> readlist n t gr -> typing_base (trvar n) (typref t) gb gr
  | apptyp : forall e1 e2 t1 t2 gb gr,
               typing_base e1 (typarr t2 t1) gb gr -> typing_base e2 t2 gb gr
               -> typing_base (tapp e1 e2) t1 gb gr
  | abstyp : forall L e t1 t2 gb gr,
               (forall x, not (termfree x L) -> not (bound x gb) -> not (termfree x e)
                  -> typing_base (open (tfvar x) e) t2 (cons (x,(t1,(fun x => False))) gb) gr)
               -> typing_base (tabs e) (typarr t1 t2) gb gr
  | pairtyp : forall e1 e2 t1 t2 gb gr,
                typing_base e1 t1 gb gr -> typing_base e2 t2 gb gr
                -> typing_base (tpair e1 e2) (typprod t1 t2) gb gr
  | letvtyp : forall L v e t1 t2 (a : abstraction) gb gr,
                value v -> typing_base v t1 gb gr -> abstr a
                -> (forall x, a x -> not (benvfree x gb))
                -> (forall x, a x -> not (renvfree x gr))
                -> (forall x, not (termfree x L) -> not (bound x gb) -> not (termfree x e)
                      -> typing_base (open (tfvar x) e) t2 (cons (x,(t1,a)) gb) gr)
                -> typing_base (tlet v e) t2 gb gr
  | letetyp : forall L e1 e2 t1 t2 (a : abstraction) gb gr,
                typing_base e1 t1 gb gr -> abstr a
                -> (forall x, a x -> not (benvfree x gb))
                -> (forall x, a x -> not (renvfree x gr))
                -> (forall x, a x -> not (dangerv x t1))
                -> (forall x, not (termfree x L) -> not (bound x gb) -> not (termfree x e2)
                      -> typing_base (open (tfvar x) e2) t2 (cons (x,(t1,a)) gb) gr)
                -> typing_base (tlet e1 e2) t2 gb gr
  | contyp : forall e t gb gr,
               typing_base e (typprod t (typlist t)) gb gr -> typing_base (tcon e) (typlist t) gb gr
.

Definition rcorrect (theta : tstore) (gb : benv) (gr : renv) :=
             length theta = length gr /\ forall n v t, readlist n v theta -> readlist n t gr
             -> typing_base v t gb gr.

Inductive typing : term -> tstore -> typ -> benv -> Prop :=
  |  rhotyp : forall e theta t gb gr, rcorrect theta gb gr -> typing_base e t gb gr
                -> typing e theta t gb
.



               (* Traduction *)

Definition BTsubstitution := var -> BTtyp.

Fixpoint BTtrans (s : BTsubstitution) (t : typ) : BTtyp :=
  match t with
  | typvar x => s x
  | typprod t1 t2 => BTprod (BTtrans s t1) (BTtrans s t2)
  | typref t0 => BTref (BTtrans s t0)
  | typlist t0 => BTlist (BTtrans s t0)
  | typarr t1 t2 => BTarr (BTtrans s t1) (BTtrans s t2)
  end.

Definition BTsubstins (s : BTsubstitution) (a : abstraction) ins :=
             fun x => If a x then ins x else s x.

Definition BTpolytrans s a t := fun t0 =>
             exists ins, BTorder (BTtrans (BTsubstins s a ins) t) t0.

Fixpoint BTbenvtrans (s : BTsubstitution) (gb : benv) : BTbenv :=
  match gb with
  | nil => nil
  | cons (x,(t,a)) gb0 => cons (x,(BTpolytrans s a t)) (BTbenvtrans s gb0)
  end.

Fixpoint BTrenvtrans (s : BTsubstitution) (gr : renv) : BTrenv :=
  match gr with
  | nil => nil
  | cons t gr0 => cons (BTtrans s t) (BTrenvtrans s gr0)
  end.





Lemma typcor : forall e t gb gr, typing_base e t gb gr -> bcorr gb.
intros; induction H; try assumption.
destruct (fresh L (BTbenvtrans (fun x => BTvar x) gb) e); destruct H1; destruct H2.
assert (not (bound x gb)).
clear H H0; intro; apply H2; clear H2; induction gb;
simpl; inversion H; constructor; apply IHgb; assumption.
assert (Hi := H0 x H1 H4 H3); inversion Hi; assumption.
Qed.

Lemma substid : forall s a, abstr a -> BTsubstins s a s = s.
intros.
apply fun_extensionality.
intro; destruct H with x.
unfold BTsubstins; rewrite (If_l (s x) (s x) H0); reflexivity.
unfold BTsubstins; rewrite (If_r (s x) (s x) H0); reflexivity.
Qed.

Lemma polytrnul : forall s a t t0, abstr a -> BTorder (BTtrans s t) t0 -> BTpolytrans s a t t0.
intros; exists s.
rewrite substid; assumption.
Qed.

Lemma btrcor : forall s gb, bcorr gb -> BTbcorr (BTbenvtrans s gb).
intros; induction H; simpl.
constructor.
constructor.
assumption.
clear H0 H1 IHbcorr; intro; apply H; clear H; induction gb;
try (destruct a0; destruct p); simpl in H0; inversion H0; constructor.
apply IHgb; assumption.
constructor.
exists (BTtrans s t).
apply polytrnul.
assumption.
apply BTorefl.
intros.
destruct H3.
exists x0.
otr t1; assumption.
Qed.

Lemma btrreadcor : forall x s a t gb, benvread x t a gb
                     -> BTbenvread x (BTpolytrans s a t) (BTbenvtrans s gb).
intros;
induction H.
constructor.
destruct u; destruct p;
constructor; apply IHbenvread; assumption.
Qed.

Lemma lrtrcor : forall s gr, length gr = length (BTrenvtrans s gr).
intros; induction gr; simpl; try rewrite IHgr; reflexivity.
Qed.

Lemma rtrreadcor : forall x s t gr, readlist x t gr -> readlist x (BTtrans s t) (BTrenvtrans s gr).
intros; induction H.
rewrite lrtrcor with s l; simpl; constructor.
simpl; constructor; assumption.
Qed.

Definition subscomp BTs s := fun x : var => BTtrans BTs (s x).

Lemma composition : forall BTs s t, BTtrans BTs (trans s t) = BTtrans (subscomp BTs s) t.
intros; induction t; simpl; try rewrite IHt1; try rewrite IHt2; try rewrite IHt;
reflexivity.
Qed.

Lemma ordtr : forall s a t t0, abstr a -> order t0 a t -> BTpolytrans s a t (BTtrans s t0).
intros; do 2 destruct H0.
exists (subscomp s x).
assert (BTsubstins s a (subscomp s x) = subscomp s x).
apply fun_extensionality; intro.
destruct H with x0.
unfold BTsubstins; rewrite (If_l (subscomp s x x0) (s x0) H2); reflexivity.
unfold BTsubstins; rewrite (If_r (subscomp s x x0) (s x0) H2).
unfold subscomp; rewrite H0; [simpl; reflexivity|assumption].
rewrite H2.
rewrite <- H1; rewrite composition.
apply BTorefl.
Qed.

Lemma trbasecor : forall s t a, abstr a -> BTpoly (BTpolytrans s a t).
intros; constructor.
exists (BTtrans s t); exists s; rewrite substid.
apply BTorefl.
assumption.
intros; destruct H1.
exists x; otr t1; assumption.
Qed.

Hint Constructors typfree.

Lemma tsubnul : forall s a ins t, abstr a -> (forall x, a x -> not (typfree x t))
                  -> BTtrans (BTsubstins s a ins) t = BTtrans s t.
intros; induction t; simpl;
try rewrite IHt; try rewrite IHt1; try rewrite IHt2; try reflexivity;
intros; try intro; try apply (H0 x H1); auto.
destruct (H n).
destruct (H0 n H1); constructor.
unfold BTsubstins; rewrite (If_r (ins n) (s n) H1); reflexivity.
Qed.

Lemma tsubcomm : forall s a a0 ins ins0 t, abstr a -> abstr a0
                   -> BTtrans (BTsubstins (BTsubstins s a ins) a0 ins0) t
                    = BTtrans (BTsubstins (BTsubstins s a0 ins0) a (BTsubstins ins a0 ins0)) t.
intros; induction t; simpl; try rewrite IHt; try rewrite IHt1; try rewrite IHt2; try reflexivity.
destruct (H n); destruct (H0 n);
unfold BTsubstins;
repeat (try (rewrite If_r; [|assumption]); try (rewrite If_l; [|assumption]));
reflexivity.
Qed.

Lemma benvsubnul : forall s a ins gb, bcorr gb -> abstr a
                     -> (forall x, a x -> not (benvfree x gb))
                     -> BTbenvtrans (BTsubstins s a ins) gb = BTbenvtrans s gb.
intros; induction gb.
simpl; reflexivity.
destruct a0; destruct p; simpl.
rewrite IHgb.
rewrite Extensionality_Ensembles
   with BTtyp (BTpolytrans (BTsubstins s a ins) a0 t) (BTpolytrans s a0 t); [reflexivity|].
unfold BTpolytrans; intro; split; intro.
destruct H2; exists x0.
rewrite tsubcomm in H2; try assumption.
rewrite tsubnul in H2; try assumption.
intros; intro; apply (H1 x1 H3);
constructor; assumption.
inversion H; assumption.
destruct H2; exists x0.
rewrite tsubcomm; try assumption.
rewrite tsubnul; try assumption.
intros; intro; apply (H1 x1 H3);
constructor; assumption.
inversion H; assumption.
inversion H; assumption.
intros; intro; apply (H1 x H2).
apply bft; assumption.
Qed.

Lemma renvsubnul : forall s a ins gr, abstr a -> (forall x, a x -> not (renvfree x gr))
                     -> BTrenvtrans (BTsubstins s a ins) gr = BTrenvtrans s gr.
intros; induction gr; simpl.
reflexivity.
rewrite IHgr.
rewrite tsubnul.
reflexivity.
assumption.
intros; intro; apply (H0 x H1); apply rfh; assumption.
intros; intro; apply (H0 x H1); apply rft; assumption.
Qed.

Hint Constructors dangerv.
Lemma BTtransbase : forall s a t, abstr a -> (forall x, a x -> not (dangerv x t))
                      -> (fun t0 : BTtyp => BTorder (BTtrans (BTsubstins s a (fun _ => BTzero)) t) t0)
                       = BTpolytrans s a t.
intros; apply Extensionality_Ensembles; intro; split; intro.
exists (fun _ : var => BTzero); assumption.
destruct H1.
destruct (BTotrans H1); apply H3.
clear H1 H2 H3.
generalize dependent x0; induction t; intros; simpl; try constructor;
try apply IHt; try apply IHt1; try apply IHt2; try assumption;
try (intros v Ha; intro; apply (H0 v Ha); auto).
destruct (H n); unfold BTsubstins; [repeat rewrite If_l|repeat rewrite If_r]; try assumption.
constructor.
apply BTorefl.
repeat rewrite tsubnul; try assumption.
apply BTorefl.
intros v Ha; intro; apply (H0 v Ha); auto.
intros v Ha; intro; apply (H0 v Ha); auto.
repeat rewrite tsubnul; try assumption.
apply BTorefl.
intros v Ha; intro; apply (H0 v Ha); auto.
intros v Ha; intro; apply (H0 v Ha); auto.
Qed.

Lemma transcor : forall e t gb gr s, typing_base e t gb gr
                   -> BTtyping_base true e (BTtrans s t) (BTbenvtrans s gb) (BTrenvtrans s gr).
intros; generalize dependent s; induction H; intros.
(* ax *)
constructor.
apply btrcor; assumption.
inversion H0; simpl; constructor.
(* fvar *)
apply BTfvartyp with (BTpolytrans s a t).
apply btrcor; assumption.
apply btrreadcor; assumption.
apply ordtr.
apply readcor with x t gb; assumption.
assumption.
(* fvar *)
apply BTrvartyp.
apply btrcor; assumption.
apply rtrreadcor; assumption.
(* app *)
apply BTapptyp with true true (BTtrans s t2); [apply IHtyping_base1|apply IHtyping_base2].
(* abs *)
apply BTabstyp with L true; intros.
simpl in H0;
replace (fun t0 : BTtyp =>
      BTorder
        ((fix BTtrans (s0 : BTsubstitution) (t : typ) {struct t} : BTtyp :=
            match t with
            | typvar x0 => s0 x0
            | typprod t3 t4 => BTprod (BTtrans s0 t3) (BTtrans s0 t4)
            | typref t3 => BTref (BTtrans s0 t3)
            | typlist t3 => BTlist (BTtrans s0 t3)
            | typarr t3 t4 => BTarr (BTtrans s0 t3) (BTtrans s0 t4)
            end) s t1) t0) with (BTpolytrans s (fun _ => False) t1).
apply H0; try assumption.
clear H H0 H1 H3 L e t1 t2 gr; intro; apply H2; clear H2; induction gb;
inversion H; constructor; apply IHgb; assumption.
apply Extensionality_Ensembles; intro; split; intro.
destruct H4.
replace (BTsubstins s (fun _ : var => False) x1) with s in H4.
assumption.
apply fun_extensionality; intro.
unfold BTsubstins; rewrite (If_r (x1 x2) (s x2)).
reflexivity.
intro; assumption.
exists s; rewrite substid.
assumption.
intro; right; intro; assumption.
(* pair *)
apply BTpairtyp with true true; [apply IHtyping_base1|apply IHtyping_base2].
(* letv *)
apply BTletvtyp with L true true (BTpolytrans s a t1).
assumption.
apply trbasecor; assumption.
intros.
destruct H6.
replace (BTbenvtrans s gb) with (BTbenvtrans (BTsubstins s a x) gb) in *.
replace (BTrenvtrans s gr) with (BTrenvtrans (BTsubstins s a x) gr) in *.
apply BTsubtyp with true (BTtrans (BTsubstins s a x) t1); [assumption|].
apply IHtyping_base.
apply renvsubnul; assumption.
apply benvsubnul; try assumption.
apply (typcor H0).
intros.
apply H5; try assumption.
intro; apply H7; clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 IHtyping_base; induction gb;
simpl; inversion H9; constructor; apply IHgb; assumption.
(* lete *)
apply BTletetyp with L true true (BTtrans (BTsubstins s a (fun x => BTzero)) t1).
replace (BTbenvtrans s gb) with (BTbenvtrans (BTsubstins s a (fun x => BTzero)) gb).
replace (BTrenvtrans s gr) with (BTrenvtrans (BTsubstins s a (fun x => BTzero)) gr).
apply IHtyping_base.
apply renvsubnul; assumption.
apply benvsubnul; try assumption.
apply (typcor H).
simpl in H5; intros.
replace (fun t0 : BTtyp =>
      BTorder (BTtrans (BTsubstins s a (fun _ : var => BTzero)) t1) t0) with (BTpolytrans s a t1).
apply H5; try assumption.
intro; apply H7; clear H H1 H2 H3 H4 H5 H6 H7 H8 IHtyping_base; induction gb;
simpl; inversion H9; constructor; apply IHgb; assumption.
rewrite BTtransbase; try assumption; reflexivity.
(* tcon *)
apply BTcontyp with true; apply IHtyping_base.
Qed.









               (* Variance *)

Inductive covariant : var -> typ -> Prop :=
  | covvar : forall x y, covariant x (typvar y)
  | covprod : forall x t1 t2, covariant x t1 -> covariant x t2
                -> covariant x (typprod t1 t2)
  | covref : forall x t, not (typfree x t) -> covariant x (typref t)
  | covlist : forall x t, covariant x t -> covariant x (typlist t)
  | covarr : forall x t1 t2, contravariant x t1 -> covariant x t2
               -> covariant x (typarr t1 t2)
with contravariant : var -> typ -> Prop :=
  | convar : forall x y, x <> y -> contravariant x (typvar y)
  | conprod : forall x t1 t2, contravariant x t1 -> contravariant x t2
                -> contravariant x (typprod t1 t2)
  | conref : forall x t, not (typfree x t) -> contravariant x (typref t)
  | conlist : forall x t, contravariant x t -> contravariant x (typlist t)
  | conarr : forall x t1 t2, covariant x t1 -> contravariant x t2
               -> contravariant x (typarr t1 t2)
.

Ltac odes := match goal with H : _ \/ _ |- _ => case H; intro; clear H end.

Ltac corev :=
match goal with
| H : covariant _ (typvar _) |- _ => clear H
| H : covariant _ (typprod _ _) |- _ => inversion H; clear H
| H : covariant _ (typref _) |- _ => inversion H; clear H
| H : covariant _ (typlist _) |- _ => inversion H; clear H
| H : covariant _ (typarr _ _) |- _ => inversion H; clear H
| H : contravariant _ (typvar _) |- _ => inversion H; clear H
| H : contravariant _ (typprod _ _) |- _ => inversion H; clear H
| H : contravariant _ (typref _) |- _ => inversion H; clear H
| H : contravariant _ (typlist _) |- _ => inversion H; clear H
| H : contravariant _ (typarr _ _) |- _ => inversion H; clear H
end.

Ltac codisc :=
match goal with
  | H : ~ covariant ?x ?t |- ~ covariant ?x (typprod ?t _) => intro; corev; apply H; assumption
  | H : ~ covariant ?x ?t |- ~ covariant ?x (typprod _ ?t) => intro; corev; apply H; assumption
  | H : typfree ?x ?t |- ~ covariant ?x (typref ?t) => intro; corev; auto
  | H : ~ covariant ?x ?t |- ~ covariant ?x (typlist ?t) => intro; corev; apply H; assumption
  | H : ~ contravariant ?x ?t |- ~ covariant ?x (typarr ?t _) => intro; corev; apply H; assumption
  | H : ~ covariant ?x ?t |- ~ covariant ?x (typarr _ ?t) => intro; corev; apply H; assumption
  | H : ?x = ?y |- ~ contravariant ?x (typvar ?y) => intro; corev; auto
  | H : ~ contravariant ?x ?t |- ~ contravariant ?x (typprod ?t _) => intro; corev; apply H; assumption
  | H : ~ contravariant ?x ?t |- ~ contravariant ?x (typprod _ ?t) => intro; corev; apply H; assumption
  | H : typfree ?x ?t |- ~ contravariant ?x (typref ?t) => intro; corev; auto
  | H : ~ contravariant ?x ?t |- ~ contravariant ?x (typlist ?t) => intro; corev; apply H; assumption
  | H : ~ covariant ?x ?t |- ~ contravariant ?x (typarr ?t _) => intro; corev; apply H; assumption
  | H : ~ contravariant ?x ?t |- ~ contravariant ?x (typarr _ ?t) => intro; corev; apply H; assumption
end.

Lemma vardec : forall x t, (covariant x t \/ not (covariant x t))
                           /\ (contravariant x t \/ not (contravariant x t)).
intros; induction t; split;
try (destruct IHt1; destruct IHt2); try destruct IHt;
try (case (diff x n); intro); try (case (tfreedec x t); intro);
try solve [repeat odes; try solve [left; constructor; assumption]; try solve [right; codisc]].
Qed.

Lemma varcase : forall x t, covariant x t -> contravariant x t -> typfree x t -> False.
intros; induction t.
inversion H1; inversion H0; destruct H6; assumption.
inversion H; inversion H0; inversion H1; [apply IHt1|apply IHt2]; assumption.
inversion H; inversion H1; apply H4; assumption.
inversion H; inversion H0; inversion H1; apply IHt; assumption.
inversion H; inversion H0; inversion H1; [apply IHt1|apply IHt2]; assumption.
Qed.

Lemma substord : forall t s s',
                   (forall x, not (covariant x t) -> not (contravariant x t) -> s x = s' x)
                   -> (forall x, typfree x t -> covariant x t -> BTorder (s x) (s' x))
                   -> (forall x, typfree x t -> contravariant x t -> BTorder (s' x) (s x))
                   -> BTorder (BTtrans s t) (BTtrans s' t).
induction t; intros; simpl.
apply H0; constructor.
(* prod *)
constructor; [apply IHt1|apply IHt2]; intros.
apply H; intro Hi; inversion Hi; [apply H2|apply H3]; assumption.
destruct (vardec x (typprod t1 t2)) as [Hcv Hcnv]; case Hcv; intro.
apply H0. apply typfprod1; assumption. assumption.
rewrite H; try apply BTorefl.
assumption. intro Hi; inversion Hi; apply varcase with x t1; assumption.
destruct (vardec x (typprod t1 t2)) as [Hcv Hcnv]; case Hcnv; intro.
apply H1. apply typfprod1; assumption. assumption.
rewrite H; try apply BTorefl.
intro Hi; inversion Hi; apply varcase with x t1; assumption. assumption.
apply H; intro Hi; inversion Hi; [apply H2|apply H3]; assumption.
destruct (vardec x (typprod t1 t2)) as [Hcv Hcnv]; case Hcv; intro.
apply H0. apply typfprod2; assumption. assumption.
rewrite H; try apply BTorefl.
assumption. intro Hi; inversion Hi; apply varcase with x t2; assumption.
destruct (vardec x (typprod t1 t2)) as [Hcv Hcnv]; case Hcnv; intro.
apply H1. apply typfprod2; assumption. assumption.
rewrite H; try apply BTorefl.
intro Hi; inversion Hi; apply varcase with x t2; assumption. assumption.
(* ref *)
assert (forall x, typfree x t -> s x = s' x).
intros; apply H; intro Hi; inversion Hi; apply H5; assumption.
assert (BTtrans s t = BTtrans s' t).
clear H H0 H1 IHt; induction t; simpl;
try rewrite IHt1; try rewrite IHt2; try rewrite IHt; try reflexivity; intros; apply H2; auto.
rewrite H3; apply BTorefl.
(* list *)
constructor; apply IHt; intros.
apply H; intro Hi; inversion Hi; [apply H2|apply H3]; assumption.
apply H0; constructor; assumption.
apply H1; constructor; assumption.
(* arr *)
constructor; [apply IHt1|apply IHt2]; intros.
rewrite H; [reflexivity| |]; intro Hi; inversion Hi; [apply H3|apply H2]; assumption.
destruct (vardec x (typarr t1 t2)) as [Hcv Hcnv]; case Hcnv; intro.
apply H1. apply typfarr1; assumption. assumption.
rewrite H; try apply BTorefl.
intro Hi; inversion Hi; apply varcase with x t1; assumption. assumption.
destruct (vardec x (typarr t1 t2)) as [Hcv Hcnv]; case Hcv; intro.
apply H0. apply typfarr1; assumption. assumption.
rewrite H; try apply BTorefl.
assumption. intro Hi; inversion Hi; apply varcase with x t1; assumption.
apply H; intro Hi; inversion Hi; [apply H2|apply H3]; assumption.
destruct (vardec x (typarr t1 t2)) as [Hcv Hcnv]; case Hcv; intro.
apply H0. apply typfarr2; assumption. assumption.
rewrite H; try apply BTorefl.
assumption. intro Hi; inversion Hi; apply varcase with x t2; assumption.
destruct (vardec x (typarr t1 t2)) as [Hcv Hcnv]; case Hcnv; intro.
apply H1. apply typfarr2; assumption. assumption.
rewrite H; try apply BTorefl.
intro Hi; inversion Hi; apply varcase with x t2; assumption. assumption.
Qed.

Lemma orcvar : forall t s s', BTorder (BTtrans s t) (BTtrans s' t)
                 -> (forall x, typfree x t -> covariant x t -> BTorder (s x) (s' x))
                    /\ (forall x, typfree x t -> contravariant x t -> BTorder (s' x) (s x)).
induction t; intros; split; intros; simpl in H.
inversion H0; assumption.
inversion H0; inversion H1; destruct H6; assumption.
inversion H; inversion H1; inversion H0;
[destruct IHt1 with s s'|destruct IHt2 with s s']; try assumption;
apply H17; assumption.
inversion H; inversion H1; inversion H0;
[destruct IHt1 with s s'|destruct IHt2 with s s']; try assumption;
apply H18; assumption.
inversion H0; inversion H1; destruct H7; assumption.
inversion H0; inversion H1; destruct H7; assumption.
inversion H; inversion H0; inversion H1; destruct IHt with s s'; try assumption.
apply H11; assumption.
inversion H; inversion H0; inversion H1; destruct IHt with s s'; try assumption.
apply H12; assumption.
inversion H; inversion H0; inversion H1;
[destruct IHt1 with s' s|destruct IHt2 with s s']; try assumption.
apply H18; assumption.
apply H17; assumption.
inversion H; inversion H0; inversion H1;
[destruct IHt1 with s' s|destruct IHt2 with s s']; try assumption.
apply H17; assumption.
apply H18; assumption.
Qed.