- Instance SystemFCa_sequent_join Γ Δ : @SequentExpansion _ _ _ _ _ (SystemFCa_sequents Γ Δ) (SystemFCa_cutrule Γ Δ) :=
- { se_expand_left := SystemFCa_left Γ Δ
- ; se_expand_right := SystemFCa_right Γ Δ }.
- admit.
- admit.
+ Instance SystemFCa_sequent_join Γ Δ : @ContextND _ _ _ _ (SystemFCa_sequents Γ Δ) :=
+ { cnd_expand_left := fun a b c => SystemFCa_left Γ Δ c a b
+ ; cnd_expand_right := fun a b c => SystemFCa_right Γ Δ c a b }.
+ (*
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ ((RArrange _ _ _ _ _ (RCossa _ _ _)))).
+ auto.
+
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))); auto.
+
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanL _))); auto.
+
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RCanR _))); auto.
+
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanL _))); auto.
+
+ intros; apply nd_rule. simpl.
+ apply (org_fc _ _ _ _ (RArrange _ _ _ _ _ (RuCanR _))); auto.
+ *)
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ Instance OrgFC Γ Δ : @ND_Relation _ (OrgR Γ Δ).
+ Admitted.
+
+ Instance OrgFC_SequentND_Relation Γ Δ : SequentND_Relation (SystemFCa_sequent_join Γ Δ) (OrgFC Γ Δ).