%{
Homework 2 (due Sept 18, 2014)
Proof Terms and Substitution
}%
term mpt: ~(A & B) => A => ~B =
fn f => fn a => fn b => f (a, b);
term disjImp: (A => C) => (B => C) => (A | B => C) =
fn f => fn g => fn d => (case d of inl a => f a | inr b => g b end);
term branch: (A & B => C) => (A | C) => (B | C) => C =
fn f => fn d1 => fn d2 =>
(case d1 of
inl a =>
case d2 of
inl b => f (a, b)
| inr c => c
end
| inr c => c
end);
term flip : (A => ~B) => (B => ~A) =
fn f => fn b => fn a => abort ((f a) b);
term demorgan : ~(A | B) => ~A & ~B =
fn f => (fn a => f (inl a), fn b => f (inr b));