- Instance SystemFCa_cutrule Γ Δ : CutRule (SystemFCa_sequents Γ Δ) :=
- { nd_cut := SystemFCa_cut Γ Δ }.
- admit.
- admit.
- admit.
- Defined.
+ Instance SystemFCa_sequents Γ Δ : @SequentND _ OrgR _ (mkJudg Γ Δ) :=
+ { snd_cut := SystemFCa_cut Γ Δ }.
+ apply Build_SequentND.
+ intros.
+ induction a.
+ destruct a; simpl.
+ apply nd_rule.
+ destruct l.
+ apply org_fc with (r:=RVar _ _ _ _).
+ auto.
+ apply nd_rule.
+ apply org_fc with (r:=RVoid _ _ ).
+ auto.
+ eapply nd_comp.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply (nd_prod IHa1 IHa2).
+ apply nd_rule.
+ apply org_fc with (r:=RJoin _ _ _ _ _ _).
+ auto.
+ admit.
+ Defined.