encrypt3.fst goes through (uses existential and indexed types fairly heavily); meanwhile, fixed a bug in tc, had omitted a free variable check in the result type of applications