+ eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
+ apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
+ (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
+ (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
+ (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).