lam 1

import data.nat
import data.list

open list

inductive In {A} : A -> list A -> Type :=
| here  {} : forall {x : A} {l : list A}
        , In x (x :: l)
| there : forall {x y : A} {l : list A}
        , In x l -> In x (y :: l)

definition notT : Type -> Type :=
    fun t, t -> empty

lemma no_In_nil A (x : A) : notT (In x nil) :=
    begin
    intros T,
    cases T,
    now
    end

inductive Maybe A :=
| None {} : Maybe A
| Some : A -> Maybe A

structure type :=
    (C : Type)
    (Lit : C -> Type)
    (arrow : C -> C -> C)
    (fuse : list C -> list C -> list C -> Prop)
    (Ix : C -> list C -> Type)

attribute type.C [coercion]

notation `~>`:60 := type.arrow

open type

inductive exp {T : type} (env : list T)
    : T -> Type :=
| var : forall {A : T}
    , Ix A env -> exp env A
| lit : forall {A : T} {l}
    , Lit A -> exp l A
| app : forall {A B}
    , exp l1 (A ~> B) -> exp l2 A -> exp l3 B
| lam : forall A {l} {B}
    , exp (t :: l) B -> exp l (A ~> B)

check unit.rec

definition untyped : type :=
{| type
, C := unit
, Lit := unit.rec Tagged
, arrrow := unit.rec unit.star
, fuse := fun unit.star unit.star unit.star := True
, Ix := In