Changeset 1964 for src/ASM/Util.ma


Ignore:
Timestamp:
May 17, 2012, 12:06:34 PM (8 years ago)
Author:
tranquil
Message:

introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1937 r1964  
    10641064  |2:
    10651065    #n' #inductive_hypothesis normalize
    1066     #absurd @inductive_hypothesis /2/
     1066    #absurd @inductive_hypothesis /2 by injective_S/
    10671067  ]
    10681068qed.
     
    14331433 #T #x #y #H @option_destruct_Some @H
    14341434qed.
     1435
     1436lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?.
     1437#A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS')
     1438qed.
     1439
     1440coercion 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.