 Timestamp:
 Dec 23, 2013, 10:23:09 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3406 r3407 446 446 [ * #H @⊥ @H % ] #H @IH assumption 447 447 qed. 448 448 449 lemma 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 (?==?) 454 normalize [* #H cases H //] #H >IH normalize // 455 qed. 456 449 457 definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ 450 458 λx.〈a_non_functional_label x,S x〉.
Note: See TracChangeset
for help on using the changeset viewer.