+lemma JSubtype_Forall_inv:
+ ∀G:list bound.∀T1,T2,T3:Typ.
+ ∀P:list bound → Typ → Prop.
+ (∀n,t1.
+ (mk_bound true n t1) ∈ G → G ⊢ t1 ⊴ (Forall T2 T3) → P G t1 → P G (TFree n)) →
+ (∀t,t1. G ⊢ T2 ⊴ t → (∀X. ¬(X ∈ fv_env G) → (mk_bound true X T2)::G ⊢ subst_type_nat t1 (TFree X) O ⊴ subst_type_nat T3 (TFree X) O)
+ → P G (Forall t t1)) →
+ G ⊢ T1 ⊴ (Forall T2 T3) → P G T1.
+ intros;
+ generalize in match (refl_eq ? (Forall T2 T3));
+ generalize in match (refl_eq ? G);
+ elim H2 in ⊢ (? ? ? % → ? ? ? % → %);
+ [1,2: destruct H6
+ |4: destruct H8
+ | lapply (H5 H6 H7); destruct; clear H5;
+ apply H;
+ assumption
+ | destruct;
+ clear H4 H6;
+ apply H1;
+ assumption
+ ]
+qed.
+
+