Changeset 1964 for src/ASM/Util.ma
 Timestamp:
 May 17, 2012, 12:06:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1937 r1964 1064 1064 2: 1065 1065 #n' #inductive_hypothesis normalize 1066 #absurd @inductive_hypothesis /2 /1066 #absurd @inductive_hypothesis /2 by injective_S/ 1067 1067 ] 1068 1068 qed. … … 1433 1433 #T #x #y #H @option_destruct_Some @H 1434 1434 qed. 1435 1436 lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?. 1437 #A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS') 1438 qed. 1439 1440 coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝ 1441 not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
Note: See TracChangeset
for help on using the changeset viewer.