Changeset 3407


Ignore:
Timestamp:
Dec 23, 2013, 10:23:09 AM (6 years ago)
Author:
sacerdot
Message:

Added get_element_append_r1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3406 r3407  
    446446[ * #H @⊥ @H % ] #H @IH assumption
    447447qed.
    448    
     448
     449lemma get_element_append_r1 :
     450 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
     451  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) →
     452   get_element ?? (l1@l2) x = get_element … l2 x.
     453#A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?)
     454normalize [* #H cases H //] #H >IH normalize //
     455qed.
     456
    449457definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
    450458λx.〈a_non_functional_label x,S x〉.
Note: See TracChangeset for help on using the changeset viewer.