Objective: provide an automated proof experience to let Catala users check two properties about their programs:

• whatever the input, the program always find at least one rule to apply for all of its variables ;
• no two unprioritized exceptions can trigger at the same time.