+(*** Type Well-Formedness judgement ***)
+
+inductive WFType : Env \to Typ \to Prop \def
+ | WFT_TFree : \forall X,G.(in_list ? X (fv_env G))
+ \to (WFType G (TFree X))
+ | WFT_Top : \forall G.(WFType G Top)
+ | WFT_Arrow : \forall G,T,U.(WFType G T) \to (WFType G U) \to
+ (WFType G (Arrow T U))
+ | WFT_Forall : \forall G,T,U.(WFType G T) \to
+ (\forall X:nat.
+ (\lnot (in_list ? X (fv_env G))) \to
+ (\lnot (in_list ? X (fv_type U))) \to
+ (WFType ((mk_bound true X T) :: G)
+ (subst_type_O U (TFree X)))) \to
+ (WFType G (Forall T U)).
+
+(*** Environment Well-Formedness judgement ***)
+
+inductive WFEnv : Env \to Prop \def
+ | WFE_Empty : (WFEnv Empty)
+ | WFE_cons : \forall B,X,T,G.(WFEnv G) \to
+ \lnot (in_list ? X (fv_env G)) \to
+ (WFType G T) \to (WFEnv ((mk_bound B X T) :: G)).
+
+(*** Subtyping judgement ***)
+inductive JSubtype : Env \to Typ \to Typ \to Prop \def
+ | SA_Top : \forall G:Env.\forall T:Typ.(WFEnv G) \to
+ (WFType G T) \to (JSubtype G T Top)
+ | SA_Refl_TVar : \forall G:Env.\forall X:nat.(WFEnv G) \to (var_in_env X G)
+ \to (JSubtype G (TFree X) (TFree X))
+ | SA_Trans_TVar : \forall G:Env.\forall X:nat.\forall T:Typ.
+ \forall U:Typ.
+ (var_bind_in_env (mk_bound true X U) G) \to
+ (JSubtype G U T) \to (JSubtype G (TFree X) T)
+ | SA_Arrow : \forall G:Env.\forall S1,S2,T1,T2:Typ.
+ (JSubtype G T1 S1) \to (JSubtype G S2 T2) \to
+ (JSubtype G (Arrow S1 S2) (Arrow T1 T2))
+ | SA_All : \forall G:Env.\forall S1,S2,T1,T2:Typ.
+ (JSubtype G T1 S1) \to
+ (\forall X:nat.\lnot (var_in_env X G) \to
+ (JSubtype ((mk_bound true X T1) :: G)
+ (subst_type_O S2 (TFree X)) (subst_type_O T2 (TFree X)))) \to
+ (JSubtype G (Forall S1 S2) (Forall T1 T2)).
+
+(*** Typing judgement ***)
+inductive JType : Env \to Term \to Typ \to Prop \def
+ | T_Var : \forall G:Env.\forall x:nat.\forall T:Typ.
+ (WFEnv G) \to (var_bind_in_env (mk_bound false x T) G) \to
+ (JType G (Free x) T)
+ | T_Abs : \forall G.\forall T1,T2:Typ.\forall t2:Term.
+ \forall x:nat.
+ (JType ((mk_bound false x T1)::G) (subst_term_O t2 (Free x)) T2) \to
+ (JType G (Abs T1 t2) (Arrow T1 T2))
+ | T_App : \forall G.\forall t1,t2:Term.\forall T2:Typ.
+ \forall T1:Typ.(JType G t1 (Arrow T1 T2)) \to (JType G t2 T1) \to
+ (JType G (App t1 t2) T2)
+ | T_TAbs : \forall G:Env.\forall T1,T2:Typ.\forall t2:Term.
+ \forall X:nat.
+ (JType ((mk_bound true X T1)::G)
+ (subst_term_tO t2 (TFree X)) (subst_type_O T2 (TFree X)))
+ \to (JType G (TAbs T1 t2) (Forall T1 T2))
+ | T_TApp : \forall G:Env.\forall t1:Term.\forall T2,T12:Typ.
+ \forall X:nat.\forall T11:Typ.
+ (JType G t1 (Forall T11 (subst_type_tfree_type T12 X (TVar O)))) \to
+ (JSubtype G T2 T11)
+ \to (JType G (TApp t1 T2) (subst_type_tfree_type T12 X T2))
+ | T_Sub : \forall G:Env.\forall t:Term.\forall T:Typ.
+ \forall S:Typ.(JType G t S) \to (JSubtype G S T) \to (JType G t T).
+
+(*** definitions about swaps ***)
+
+let rec swap_Typ u v T on T \def
+ match T with
+ [(TVar n) \Rightarrow (TVar n)
+ |(TFree X) \Rightarrow (TFree (swap u v X))
+ |Top \Rightarrow Top
+ |(Arrow T1 T2) \Rightarrow (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
+ |(Forall T1 T2) \Rightarrow (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
+
+definition swap_bound : nat \to nat \to bound \to bound \def
+ \lambda u,v,b.match b with
+ [(mk_bound B X T) \Rightarrow (mk_bound B (swap u v X) (swap_Typ u v T))].
+
+definition swap_Env : nat \to nat \to Env \to Env \def
+ \lambda u,v,G.(map ? ? (\lambda b.(swap_bound u v b)) G).
+
+(****** PROOFS ********)
+
+lemma subst_O_nat : \forall T,U.((subst_type_O T U) = (subst_type_nat T U O)).
+intros;elim T;simplify;reflexivity;
+qed.
+
+(*** theorems about lists ***)
+
+(* FIXME: these definitions shouldn't be part of the poplmark challenge
+ - use destruct instead, when hopefully it will get fixed... *)
+
+lemma inj_head : \forall h1,h2:bound.\forall t1,t2:Env.
+ ((h1::t1) = (h2::t2)) \to (h1 = h2).
+intros.
+lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption.