path: root/test-suite/output/Cases.out

t_rect = 
[P:(t ->Type); f:([x:=t](x0:x)(P x0) ->(P (k x0)))]
 Fix F
   {F [t:t] : (P t) := <[t0:t](P t0)>Cases t of (k x x0) => (f x0 (F x0)) end}
     : (P:(t ->Type))([x:=t](x0:x)(P x0) ->(P (k x0))) ->(t:t)(P t)