fact: Fixpoint fv_ee (e : exp) {struct e} : atoms := match e with | exp_bvar i => {} | exp_fvar x => {{ x }} | exp_abs V e1 => (fv_ee e1) | exp_app e1 e2 => (fv_ee e1) `union` (fv_ee e2) | exp_tabs V e1 => (fv_ee e1) | exp_tapp e1 V => (fv_ee e1) | exp_let e1 e2 => (fv_ee e1) `union` (fv_ee e2) | exp_inl e1 => (fv_ee e1) | exp_inr e1 => (fv_ee e1) | exp_case e1 e2 e3 => (fv_ee e1) `union` (fv_ee e2) `union` (fv_ee e3) end.
imports: Fsub.Fsub_LetSum_Definitions