-inductive JSubtype : (list bound) \to Typ \to Typ \to Prop \def
- | SA_Top : \forall G.\forall T:Typ.(WFEnv G) \to
- (WFType G T) \to (JSubtype G T Top)
- | SA_Refl_TVar : \forall G.\forall X:nat.(WFEnv G)
- \to (in_list ? X (fv_env G))
- \to (JSubtype G (TFree X) (TFree X))
- | SA_Trans_TVar : \forall G.\forall X:nat.\forall T:Typ.
- \forall U:Typ.
- (in_list ? (mk_bound true X U) G) \to
- (JSubtype G U T) \to (JSubtype G (TFree X) T)
- | SA_Arrow : \forall G.\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.\forall S1,S2,T1,T2:Typ.
- (JSubtype G T1 S1) \to
- (\forall X:nat.\lnot (in_list ? X (fv_env G)) \to
- (JSubtype ((mk_bound true X T1) :: G)
- (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O))) \to
- (JSubtype G (Forall S1 S2) (Forall T1 T2)).
-
-notation "hvbox(e ⊢ break ta ⊴ break tb)"
+inductive JSubtype : list bound → Typ → Typ → Prop ≝
+ | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
+ | SA_Refl_TVar : ∀G,X.WFEnv G → in_list ? X (fv_env G)
+ → JSubtype G (TFree X) (TFree X)
+ | SA_Trans_TVar : ∀G,X,T,U.in_list ? (mk_bound true X U) G →
+ JSubtype G U T → JSubtype G (TFree X) T
+ | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 →
+ JSubtype G (Arrow S1 S2) (Arrow T1 T2)
+ | SA_All : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 →
+ (∀X.¬ (in_list ? X (fv_env G)) →
+ JSubtype ((mk_bound true X T1) :: G)
+ (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
+ JSubtype G (Forall S1 S2) (Forall T1 T2).
+
+notation "mstyle color #007f00 (hvbox(e ⊢ break ta ⊴ break tb))"