• Theorem incl_nil
• Tactic incl_tac_rec
• Tactic incl_tac
• Tactic in_tac
• Examples