Fix #10757: Program Fixpoint uses "exists" for telescopes

This helps extraction by not building sigT which can lower to Prop by
template polymorphism.

Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.

In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.

We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.

0 files changed, 0 insertions, 0 deletions