Changeset 1930 for src/utilities
 Timestamp:
 May 9, 2012, 6:30:41 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extralib.ma
r1882 r1930 114 114 qed. 115 115 116 (* Replace decision functions by result. *) 117 118 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f. 119 #P #f #p #Q #H cases f; 120 [ @H 121  #np cut False [ @(absurd ? p np)  * ] 122 ] qed. 123 124 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f. 125 #P #f #p #Q #H cases f; 126 [ #np cut False [ @(absurd ? np p)  * ] 127  @H 128 ] qed. 129 130 116 131 lemma not_exists_forall: 117 132 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
Note: See TracChangeset
for help on using the changeset viewer.