diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-01 15:21:37 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-01 15:21:37 -0500 |
commit | 3bca0281034722fbbd3a45b16ae841ef54c317ca (patch) | |
tree | 0c123466bbd638dd4f9f7e677849202467b25db9 /theories/Init/Specif.v | |
parent | bdc74cd1b945b69f81264cb6df8eb793c0c6817f (diff) |
Remove some trailing whitespace in Init/Specif.v
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r-- | theories/Init/Specif.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 9fc00e80c..e94b2e346 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P of an [a] of type [A], a of a proof [h] that [a] satisfies [P], and a proof [h'] that [a] satisfies [Q]. Then [(proj1_sig (sig_of_sig2 y))] is the witness [a], - [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and [(proj3_sig y)] is the proof of [(Q a)]. *) Section Subset_projections2. @@ -263,10 +263,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. |