%% Convert a natural deduction proof into to sequent calculus proof
%%
%% We consider a logic with just impliciation

Define convert nil nil.
Define convert (nd G :: L) (hyp G :: K) := convert L K.

Theorem convert_member : forall L K H,
  convert L K -> member (nd H) L -> member (hyp H) K.
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H4 H3. search.

Theorem nd_to_seq_ext : forall L K G,
  {L |- nd G} -> convert L K -> {K |- conc G}.
induction on 1. intros. case H1.
  apply convert_member to H2 H3. search.
  apply IH to H3 _. search.
  apply IH to H3 H2. apply IH to H4 H2. search.

Theorem nd_to_seq : forall G, {nd G} -> {conc G}.
intros. apply nd_to_seq_ext to H1 _. search.