* TODO Prototype code [4/4]
     - [X] small cleanup of the code of the implementation
     - [X] bring the changes from the test branch and the fixes for
       the bug in a new PR
     - [X] rename Node to Switch in the code so that it coherent with the
       workshop submission
     - [X] finish the code for handling variables
     - [ ] Put a reasonable readme
* TODO Workshop [2/2]:
     - [X] write the part about equivalence checking in the submission
     - [X] explain why the judgment on equivalence is not symmetric
     - [ ] Reread and submit
* TODO Proof [1/6]:
   - [ ] define covering of C_S
   - [X] define running a value against source/target/trees
   - [ ] be clearer about handling of guards
   - [ ] be clearer about handling of or-patterns
         this could be left at the end
   - [ ] finish the case analysis on p₀ⱼ (matrix decomposition)
   - [ ] revisit point case analysis of equivalence checking, point 4, YES
     subcase:
         in the forall we either forgot the fallback case
         (that should be easy to generalize and move with the rest)
         or I forgot something about k_i because it seems out of place