gistfile1.md

ac

Goal:

◊ ≫
  ∩(U<0>; A.
  ∩(U<0>; B.
  ∩(∏(A; _.∏(B; _.U<0>)); Q.
  ∏(∏(A; a.prod(B; b.ap(ap(Q; a); b))); _.
  prod(∏(A; _.B); f.∏(A; a.ap(ap(Q; a); ap(f; a))))))))

Evidence:

isect-intro(A.isect-intro(B.isect-intro(Q.fun-intro(x.prod-intro(λ(z.spread(ap(x; z); u._.u)); lam=(x'.spread=(ap=(hyp=(x); hyp=(x')); s._._.hyp=(s)); hyp=(A)); fun-intro(_.<<<<<ADMIT>>>>>; hyp=(A))); fun=(hyp=(A); a.prod=(hyp=(B); b.ap=(ap=(hyp=(Q); hyp=(a)); hyp=(b))))); fun=(cum(hyp=(A)); _.fun=(cum(hyp=(B)); _.univ=))); univ=); univ=)

Extract:

λ(x.pair(λ(z.spread(ap(x; z); u._.u)); λ(_.<<<<<ADMIT>>>>>)))