λP2 = λC : Who Needs Type Constructors
This is an attempt to prove an injective map from the Calculus of Constructions to System λP2 from the lambda cube.
This is an attempt to prove an injective map from the Calculus of Constructions to System λP2 from the lambda cube.