LogicalFoundations Unfinished Poly.v Define exp for church encoded numbers Tactics.v Additional Exercises Logic.v Prove equivalent excluded middle definition IndProp.v ev_plus_plus R_equiv_fR MStar'' pumping Additional Exercises ProofObjects.v leibniz_equality__equality