Sequent modeling attempts

gistfile1.txt

(\g \h -> 
 (\x -> [[apply 'g 'x] = 'h]) = (\x -> ['g = [lambda 'x 'h]]))

-- x is dynamically bound above; usages of this property will have x free in h. 
-- Not sufficient, I think.

-- Here's a (rather verbose) way to define (er, assume) W = \x. x x

\W (x -> ['W apply 'x] = ['x apply x'])

-- We can encode more complex lambdas by chaining these propositions.  But it looks like
-- for each variable in the term language, we have to have a variable in the encoding.
-- That's fine, but variables are not "first class", which may make working with terms
-- difficult.  A lambda is a "first class variable" in some sense, so it may make sense
-- to build in lambdas and the beta rules.  Should we be so cavalier as to auto-normalize
-- all terms?  Anyway the beta rule is approximately as complex as the equality rule, and
-- we can encode the latter using the former. 


(A :[Set of 'X] -> A :Set)

(\X :Set
 \x :X
 -> 
 [['x in 'X] : Prop]
)

(\x \X -> [['x not in 'X] = [not ['x in 'X]])

(\P \Q :Prop ->
 [['P or 'Q] = '(\Z :Prop (P -> Z) (Q -> Z) -> Z)]]

( \A :Type 
  \X :[Set of 'A]
  -> 
  (\x :A -> [['x in 'X] or ['x not in 'X]])
  \elems :[List of 'A]
)

 
Env :Type    -- ['Env : 'Type]
(e :Env -> A :Set (a :A -> a :Object ['a in 'e]))