inria-internship /
* 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
         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