fact: Fixpoint computes {A} (tau : TT A) {struct tau}: A -> L.term -> Type := match tau with !_ => fun x xInt => (xInt = enc x) | @TyArr A B tau1 tau2 => fun f t_f => proc t_f * forall (a : A) t_a, computes tau1 a t_a -> {v : term & (app t_f t_a >* v) * computes tau2 (f a) v} end%type.
imports: String