[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear all, The conversion rule of the Calculus of Constructions (CC) is usually defined as follows: G |- e : A G |- A : s A ==beta B ------------------- Conv G |- e : B I wonder if this rule is equivalent to the one using *one-step* beta reduction: G |- e : A G |- A : s A --> B \/ B --> A -------------------------- Conv-Step G |- e : B This "Conv-Step" rule is shown in Geuvers' paper [1, Definition 4.1] but which never mentions if it is equivalent to the original "Conv" rule. So, my question is: has it ever been proved that the two conversion rules are equivalent? If so, what is the appropriate article to refer to for this proof? Thanks a lot! Sincerely, Yanpeng [1] Geuvers, Herman. "A short and flexible proof of Strong Normalization for the Calculus of Constructions." International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 1994. URL: http://flint.cs.yale.edu/trifonov/cs629/Geuvers-SN-CC-2up.ps
