changes:
- created "paths" into cotrees;
- allowed for construction of cotree_exists based on path evidence;
- proved that 1/1 and 2/1 are in the calkin-wilf tree.
- set up form of proof for "forall q:Q, (reduce q) in calkin_wilf";

Signed-off-by: Pepijn Kokke <pepijn.kokke@gmail.com>