I have extended Lambda calculus using Coq proof assistant to implement a core language that includes two Python language features (compound comparison statement and generator function). I have also described the syntax, operational semantics and type system of the features.