+ Implicit Arguments RURule [[Γ][Δ][h][c]].
+
+ Context (ndr_systemfc:@ND_Relation _ Rule).
+
+ (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
+ (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
+ (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
+ Inductive Rule_PCF {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=
+ | PCF_RCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a ))
+ | PCF_RCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a ))
+ | PCF_RuCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a ))
+ | PCF_RuCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a ))
+ | PCF_RAssoc : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RAssoc t a b c ))
+ | PCF_RCossa : ∀ t a b c , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCossa t a b c ))
+ | PCF_RLeft : ∀ h c x , Rule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
+ | PCF_RRight : ∀ h c x , Rule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
+ | PCF_RExch : ∀ t a b , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RExch t a b ))
+ | PCF_RWeak : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RWeak t a ))
+ | PCF_RCont : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCont t a ))
+
+ | PCF_RLit : ∀ Σ τ , Rule_PCF [ ] [_>>_>_|-_] (RLit Γ Δ Σ τ )
+ | PCF_RNote : ∀ Σ τ l n , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RNote Γ Δ Σ τ l n)
+ | PCF_RVar : ∀ σ l, Rule_PCF [ ] [_>>_>_|-_] (RVar Γ Δ σ l)
+ | PCF_RLam : ∀ Σ tx te q , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLam Γ Δ Σ tx te q )
+ | PCF_RApp : ∀ Σ tx te p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RApp Γ Δ Σ tx te p l)
+ | PCF_RLet : ∀ Σ σ₁ σ₂ p l, Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RLet Γ Δ Σ σ₁ σ₂ p l)
+ | PCF_RBindingGroup : ∀ b c d e , Rule_PCF ([_>>_>_|-_],,[_>>_>_|-_]) [_>>_>_|-_] (RBindingGroup _ _ b c d e)
+ | PCF_REmptyGroup : Rule_PCF [ ] [_>>_>_|-_] (REmptyGroup _ _ ).
+
+(* | PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ lev , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).*)
+ Implicit Arguments Rule_PCF [ ].