annotated proof indirect : A & (A & A => B) => B = begin [ u : A & (A & A => B); fst u : A; snd u : A & A => B; [ w : A; (w, w) : A & A; (snd u) (w, w) : B ]; fn w => (snd u) (w, w) : A => B; (fn w => (snd u) (w, w)) (fst u) : B ]; fn u => (fn w => (snd u) (w, w)) (fst u) : A & (A & A => B) => B end; % Note that the type annotation is necessary for the redundant term term indirect_term : A & (A & A => B) => B = fn u => ((fn w => (snd u) (w, w)) : A => B) (fst u); annotated proof direct : A & (A & A => B) => B = begin [ u : A & (A & A => B); fst u : A; (fst u, fst u) : A & A; snd u : A & A => B; (snd u) (fst u, fst u) : B]; fn u => (snd u) (fst u, fst u) : A & (A & A => B) => B end; term direct_term : A & (A & A => B) => B = fn u => (snd u) (fst u, fst u);