| ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
| ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
| EEsc Γ Δ ξ ec t lev e => expr2antecedent e
| ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
| ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
| EEsc Γ Δ ξ ec t lev e => expr2antecedent e