Index of concepts for Week 06

• _ 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)
• exists (among the assumptions)
• ex_intro (tCPA tactic)
• intro, with one argument (tCPA tactic, revisited)
• intros, destructuring (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)
• 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

Created [22 Feb 2024]