Close Scope nat_scope. Open Scope type_scope. Inductive Stoup := None | One. Definition StoupSem (S : Stoup) := match S with | None => Empty_set | One => unit end. Record StCtx X := mkStCtx { S : Stoup; ty : StoupSem S -> X }. Definition cdot {X} : StCtx X := mkStCtx _ None (fun x => match x with end). Definition hstoup {Y} (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end). Inductive VType : Set := VUnit : VType | VTimes : forall (A A' : VType), VType | VU : forall (B : CType), VType with CType : Set := | CTo : forall (A : VType) (B : CType), CType | CF : forall (A : VType), CType. Inductive Vlt : VType -> VType -> Set := vrefl : forall A, Vlt A A | vtrans : forall A1 A2 A3, Vlt A1 A2 -> Vlt A2 A3 -> Vlt A1 A3 | vtimesmon : forall A1 A1' A2 A2', Vlt A1 A2 -> Vlt A1' A2' -> Vlt (VTimes A1 A1') (VTimes A2 A2') | vumon : forall B1 B2, Clt B1 B2 -> Vlt (VU B1) (VU B2) with Clt : CType -> CType -> Set := crefl : forall B, Clt B B | ctrans : forall B1 B2 B3, Clt B1 B2 -> Clt B2 B3 -> Clt B1 B3 | ctimesmon : forall A1 A2 B1 B2, Vlt A1 A2 -> Clt B1 B2 -> Clt (CTo A1 B1) (CTo A2 B2) | cfmon : forall A1 A2, Vlt A1 A2 -> Clt (CF A1) (CF A2) . Definition Vars := Set. (* Definition VCtx (U : Vars) := U -> VType. *) Record VCtx := mkVCtx { U : Vars; vty : U -> VType }. Definition ext (G : VCtx) (A : VType) : VCtx := mkVCtx (U G + unit) (fun x => match x with | inl x => vty G x | inr tt => A end). Definition CCtx := StCtx CType. Inductive Value : VCtx -> VType -> Type := | var : forall G (x : U G), Value G (vty G x) | vunit : forall G, Value G VUnit | vpair : forall {G} A A' (v : Value G A) (v' : Value G A'), Value G (VTimes A A') | vdestr : forall {G} A A' Am (v : Value G (VTimes A A')) (vk : Value (ext G A) Am) (vk' : Value (ext G A') Am), Value G Am | vthunk : forall {G} B (M : Term G cdot B), Value G (VU B) with Term : VCtx -> CCtx -> CType -> Type := | hole : forall G B, Term G (hstoup B) B | lambda : forall {G Dt B} A (M : Term (ext G A) Dt B), Term G Dt (CTo A B) | app : forall {G Dt A B} (M : Term G Dt (CTo A B)) (v : Value G A), Term G Dt B | force : forall {G B} (v : Value G (VU B)), Term G cdot B | ret : forall {G A} (v : Value G A), Term G cdot (CF A) | lett : forall {G Dt A B} (M : Term G Dt (CF A)) (N : Term (ext G A) cdot B), Term G Dt B .