Implement #Bool/induction in impredicative setoid encoding

[nponeccop]

Basically, a function from proofs of P true and P false to a proof of forall x : Bool . P x

[nponeccop]

See http://nponeccop.livejournal.com/480539.html but there are questons

[nponeccop]

It turned out that "normal" Bool eliminator is impossible. So this task becomes essentially the task of implementing the impredicative setoid-based encoding (which didn't exist before as a separate task).

Blocked by #30

[5HT]

$ time (./om print type a "#Data/Bool/induc" , mode "posets" > /dev/null)

real 0m1.055s
user 0m0.962s
sys 0m0.291s