# HG changeset patch # User Adam Chlipala # Date 1221063414 14400 # Node ID 77e1a7eda0b8c92227af002d2ba6f8864b12c93c # Parent 1a82839f83b7a0bcbfa2f83c5df628bae9f74e31 Little fixes diff -r 1a82839f83b7 -r 77e1a7eda0b8 src/InductiveTypes.v --- a/src/InductiveTypes.v Mon Sep 08 16:00:02 2008 -0400 +++ b/src/InductiveTypes.v Wed Sep 10 12:16:54 2008 -0400 @@ -87,7 +87,7 @@ destruct 1. Qed. -(** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and dependent function types.) +(** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and implication. An implication is just a quantification over a proof, where the quantified variable is never used. It generally makes more sense to refer to implication hypotheses by number than by name, and Coq treats our quantifier over an unused variable as an implication in determining the proper behavior.) We can see the induction principle that made this proof so easy: *)