| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
| RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
| RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
- | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
+ | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
| RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
| RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
| RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
- | RJoin Γ p lri m x q l => let case_RJoin := tt in _
| RVoid _ _ l => let case_RVoid := tt in _
| RBrak Σ a b c n m => let case_RBrak := tt in _
| REsc Σ a b c n m => let case_REsc := tt in _
apply ileaf in X. simpl in X.
apply X.
- 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.
-
destruct case_RApp.
apply ILeaf.
inversion X_.
apply X0'.
destruct case_RCut.
+ apply rassoc.
+ apply swapr.
+ apply rassoc'.
+
inversion X_.
subst.
clear X_.
+
+ apply rassoc' in X0.
+ apply swapr in X0.
+ apply rassoc in X0.
+
induction Σ₃.
destruct a.
subst.