Test cases for type inference

[fehrenbach]

[fehrenbach]

Test substitution in lambda case of typecheck push with known result type: > test: Pi s : * . s -> s = lambda t : * . lambda x : t . x ;

Find a term that tests the same with inference.