← All problems
Unverified
Expansion Postponement for Pure Type Systems
Replace the usual conversion rule of a Pure Type System by separate contraction and expansion rules. Expansion Postponement is the assertion that every derivable judgement has a derivation using the expansion rule at most once, and then only as the final inference. Does Expansion Postponement hold for every Pure Type System?
