Made quite some progress but also found out some things are going to be really
complex to prove. For instance, we need to start proving properties about
intersections and unions of environments in order to proof correctness for
and and or.