gistfile1.txt

Fixpoint subst_exp {b} (e : exp_ b) {struct e} : list (var * exp_ b) -> exp_ b :=
    match e with
    | e_var v => fun E =>
        match Metatheory.get v E with
        | Some e' => e'
        | None => e_var v
        end
    | e_field e0 f => fun E => e_field (subst_exp e0 E) f
    | e_meth e0 m es => fun E => e_meth (subst_exp e0 E) m (List.map (fun e => subst_exp e E) es)
    | e_new C es => fun E => e_new C (List.map (fun e => subst_exp e E) es)
    | e_cast C e => fun E => e_cast C (subst_exp e E)
    | e_lib => fun _ => e_lib
    end.