diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 72758ffe0..d93bbbac1 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -92,9 +92,16 @@ Notation Snd := (snd ? ?). ]. Hints Resolve pair inl inr : core v62. -Lemma surjective_pairing : (A,B:Set;H:A*B)H=(pair A B (Fst H) (Snd H)). +Lemma surjective_pairing : (A,B:Set;p:A*B)p=(pair A B (Fst p) (Snd p)). Proof. -NewDestruct H; Reflexivity. +NewDestruct p; Reflexivity. +Qed. + +Lemma injective_projections : + (A,B:Set;p1,p2:A*B)(Fst p1)=(Fst p2)->(Snd p1)=(Snd p2)->p1=p2. +Proof. +NewDestruct p1; NewDestruct p2; Simpl; Intros Hfst Hsnd. +Rewrite Hfst; Rewrite Hsnd; Reflexivity. Qed. V7only[ |