fact: Definition memo_get_val n (v: memo_val): A n := match v with | memo_mval m x => match is_eq n m with | left H => match H in (eq _ y) return (A y -> A n) with | eq_refl => fun v1 : A n => v1 end | right _ => fun _ : A m => f n end x end.
imports: Eqdep_dec Streams