- destruct case_RJoin.
- apply ILeaf; simpl; intros.
- inversion X_.
- apply ileaf in X.
- apply ileaf in X0.
- simpl in *.
- destruct vars; inversion H.
- destruct o; inversion H3.
- refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
- apply FreshMon.
- apply FreshMon.
- apply IBranch; auto.
-