lambda-C

Example 1
context:
prop:*; impl:prop->prop->prop; T:prop->*; implin: @p,q:prop.((T p)->(T q))->(T(impl p q)); implel: @p,q:prop.(T(impl p q))->(T p)->(T q)

prove:
a) refl: @p:prop.T(impl p p)
b) trans: @p,q,r:prop.(T(impl p q))->(T(impl q r))->(T(impl p r))
Example 2
context:
false=@p:*.p; exfalso:@p:*.false->p; not=\p:*.p->false

prove:
a) a: @p,q:*.(p->q)->(not q)->(not p)
b) b: @p:*.p->(not(not p))
c) c: @p:*.(not(not(not p)))->(not p)

add to context: classic:@p:*.(not(not p))->p
(hint for d and e: after 'intros' do 'apply classic')
d) d: @p,q:*.((not q)->(not p))->(p->q)
e) e: @p,q:*.((p->q)->p)->p