Add coinductive helper theorems for cyclic itree structures and bisimulation

[daole2904]

Occasionally, when doing proofs on itrees, we want to specify cases where, after stepping through some nodes (Ret or Tau) of an itree, we meet another concrete tree, or a tree structure. This PR add coinductive definitions and helper theorems for:

• ret_or_reach: After stepping through some nodes, we arrive at a concrete tree.
• ret_or_reach_abs: After stepping through some nodes, we arrive at an initialised tree from the abs structure.
• strong_bisim_upfrom: Specifying two trees that are strongly bisimulating each other starting from some concrete point up to the whole tree.
• strong_bisim_upfrom_abs: Similar to the above, but starting from some initialised tree from the abs structure.
• weak_bisim_upfrom, weak_bisim_upfrom_abs: weakly bisimulation version of the above ones.

Note: I think this can be considered as "bisimulation up to some context" where the context is the abstracted structure abs.

Also added some additional theorems for doing proofs with itrees.