تمرین ۷ (۱۶ اردیبهشت): تمرین (t_update_permute) از فصل Maps.v و (plus_one_r') و (byntree_ind) از فصل IndPrinciples.v
تمرین ۶ (۹ اردیبهشت): تمرین های (double_neg_inf) (contrapositive) (or_distributes_over_and) (dist_not_exists)(All) (combine_odd_even)(All_forallb)(excluded_middle_irrefutable)(not_exists_dist) از فصل Logic.v و تمرینهای (ev_ev__ev) (R_provability) (reflect_iff) (beq_natP_practice) (nostutter_defn) از فصل IndProp.v
تمرین ۵ (۲۶ فروردین): تمرینهای silly_ex apply_exercise1 apply_with_exercise plus_n_n_injective beq_nat_true gen_dep_practice combine_split destruct_eqn_practice forall_exists_challenge از فصل Tactics.v
تمرین ۴: (۱۹ فروردین) همهی تمرینهای Lists.v و Poly.v
