prop : type.    %name prop A.
top : prop.
imp : prop -> prop -> prop.
and : prop -> prop -> prop.

% hypotheses
hyp : prop -> type.

% G |- C
conc : prop -> type.

init : hyp A -> conc A.
topR : conc top.
andL : (hyp A -> hyp B -> conc C) ->
       (hyp (and A B) -> conc C).
andR : conc A -> conc B ->
       conc (and A B).
impL : conc A -> (hyp B -> conc C) ->
       (hyp (imp A B) -> conc C).
impR : (hyp A -> conc B) ->
       conc (imp A B).

cut : {A: prop} 
      {D: conc A}
      {E: hyp A -> conc C}
      {F: conc C}
      type.
%mode cut +A +D +E -F.

initD : cut A (init Ha) ([Ha] E Ha) (E Ha).

initE : cut A D ([Ha] init Ha) D.
closed : cut A D ([Ha] E') E'.

andC : cut (and A B) (andR D1 D2) ([Hab : hyp (and A B)] andL ([Ha : hyp A] [Hb : hyp B] E' Hab Ha Hb) Hab) F
    <- ({Ha} {Hb} cut (and A B) (andR D1 D2) ([Hab] E' Hab Ha Hb) (F1 Ha Hb))
    <- ({Hb} cut A D1 ([Ha] F1 Ha Hb) (F2 Hb))
    <- cut B D2 ([Hb] F2 Hb) F.

impC : cut (imp A B) (impR ([Ha] D' Ha))
           ([Hab] impL (E1 Hab : conc A) ([Hb] E2 Hab Hb : conc C) Hab)
           F
    <- cut (imp A B) (impR D') E1 (F1 : conc A)
    <- ({Hb:hyp B} cut (imp A B) (impR D') ([Hab] E2 Hab Hb) (F2 Hb : conc C))
    <- cut A F1 D' (F3 : conc B)
    <- cut B F3 F2 F.

andLLC : cut A (andL ([Ha][Hb] D' Ha Hb) Hab) E 
               (andL ([Ha][Hb] F' Ha Hb) Hab)
      <- ({Ha}{Hb} cut A (D' Ha Hb) E (F' Ha Hb)).

impLLC : cut A (impL D1 ([Hb] D2 Hb) Hi) E
               (impL D1 F2 Hi)
      <- ({Hb} cut A (D2 Hb) E (F2 Hb)).

andRRC : cut A D ([Ha] andR (E1 Ha) (E2 Ha)) (andR F1 F2)
      <- cut A D E1 F1
      <- cut A D E2 F2.

impRRC : cut A D ([Ha] impR ([H1] E1 Ha H1)) (impR ([H1] F1 H1))
      <- ({H1} cut A D ([Ha] E1 Ha H1) (F1 H1)).

andLRC : cut A (D : conc A) ([Ha] andL ([H1] [H2] E' Ha H1 H2) Hp)
                            (andL ([H1][H2] F' H1 H2) Hp)
      <- ({H1}{H2} cut A D ([Ha] E' Ha H1 H2) (F' H1 H2)).

impLRC : cut A (D : conc A) ([Ha] impL (E1 Ha) ([Hb] E2 Ha Hb) Hi)
                            (impL F1 ([Hb] F2 Hb) Hi)
      <- cut A D ([Ha] E1 Ha) F1
      <- ({Hb} cut A D ([Ha] E2 Ha Hb) (F2 Hb)).

%block hyp : some {A : prop} block {H : hyp A}.
%worlds (hyp) (cut _ _ _ _).

%total {A [D E]} (cut A D E F).