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