Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3549 r3552 821 821 *: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH 822 822 ] 823 qed.824 825 let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝826 (match l return λx.l=x → ? with827 [ nil ⇒ λ_.nil ?828  cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)829 ])(refl …).830 [ >prf %%  >prf %2 assumption]831 qed.832 833 lemma dependent_map_append : ∀A,B,l1,l2,f.834 dependent_map A B (l1 @ l2) (λa,prf.f a prf) =835 (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).836 [2: @hide_prf /2/  3: @hide_prf /2/]837 #A #B #l1 elim l1 normalize /2/838 qed.839 840 lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.841 ∀EQ:l1 = l2.842 dependent_map A B l1 (λa,prf.f a prf) =843 dependent_map A B l2 (λa,prf.f a ?).844 [2: >EQ //  #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]845 823 qed. 846 824
Note: See TracChangeset
for help on using the changeset viewer.