fetburner

Require Import Autosubst.Autosubst.
Require Import Arith List Omega Program Relations.

Inductive type :=
  | Top
  | Arrow (S T : type)
  | Inter (S T : type).

Inductive sub : type -> type -> Prop :=
  | S_Refl T : sub T T

ekmett

{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language TypeFamilies #-}
{-# language RankNTypes #-}
{-# language NoImplicitPrelude #-}
{-# language FlexibleContexts #-}
{-# language MultiParamTypeClasses #-}
{-# language GADTs #-}
{-# language ConstraintKinds #-}