Type theory and functional programming
Simon Thompson · Kent Academic Repository (University of Kent) · 1991
We shall see further examples of the use of labels after seeing the rule for implication elimination. ⇒ EliminationFrom proofs of the formulas A and A ⇒ B we can infer the formula B. The assumptions upon which the proof of B depends are those of the proofs of A and A ⇒ B combined.The rule is writtenNow we can consider a more complicated example,