Index of concepts for Week 07

• _ at _ (tCPA keyword, revisited)
• _ in _ (tCPA keyword, revisited)
• clear
• completeness (of an equality predicate)
• completeness (of an equality predicate, the remaining case)
• Corollary (tCPA keyword, revisited)
• Definition (tCPA keyword, revisited)
• eqn (tCPA keyword, revisited)
• Eureka lemma (revisited)
• exists (among the assumptions)
• ex_intro (tCPA tactic)
• intro, with one argument (tCPA tactic, revisited)
• intros, deconstructing (tCPA tactic, revisited)
• intros, with several arguments (tCPA tactic, revisited)
• isomorphism (type)
• Lemma (tCPA keyword, revisited)
• Proof (tCPA keyword, revisited)
• Property (tCPA keyword, revisited)
• Proposition (tCPA keyword, revisited)
• Qed (tCPA keyword, revisited)
• Restart (tCPA keyword, revisited)
• revert, with one argument (tCPA tactic, revisited)
• revert, with several arguments (tCPA tactic, revisited)
• ring (tCPA tactic)
• routine proof
• soundness (of an equality predicate)
• soundness (of an equality predicate, the remaining case)
• Check (tCPA command, revisited)
• Compute (tCPA command, revisited)
• Search (tCPA command, revisited)
• Theorem (tCPA keyword, revisited)

Version

Moved the entry for the ring tactic from Week 10 [05 Jun 2025]

Created [07 Mar 2025]