Require Natural.
Require Extraction.

Section SetA.
Variable A : Set.
Inductive List : Set := 
           nil : List 
        | cons : A -> List -> List.
Token "::".
Infix 1 "::" cons.



Inductive catP : List -> List -> List -> Prop :=
      catP_nil : (l2:List) (catP nil l2 l2)
   | catP_cons : (l,l2,lt:List)(x:A) (catP l l2 lt) -> 
                 (catP (cons x l) l2 (cons x lt)).

Hint catP_nil catP_cons.



Theorem proofCat : (l1,l2:List) (Ex [l:List] (catP l1 l2 l)).

Induction l1; Clear  l1; Intros.
Exists  l2.
Auto.
Elim (H l2); Clear  H.
Intros x H.
Exists  (cons a x).
Elim H; Clear  H.
Auto.
Auto.

Save.


Print Natural proofCat.


Check (l1,l2:List) { l:List |  (catP l1 l2 l) }.

Theorem progCat : (l1,l2:List) { l:List |  (catP l1 l2 l) }.
 (* ............. *)
Induction l1; Clear  l1; Intros.
Exists  l2.
Auto.
Elim (H l2); Clear  H.
Intros x H.
Exists  (cons a x).
Elim H; Clear  H.
Auto.
Auto.

Save.



Extraction progCat.


Write Caml File "cat" [progCat].

Save State s1.
End SetA.


Write Caml File "cat" [progCat].
Restore State s1.


Fixpoint cat [l1:List] : List -> List := 
    [l2:List] 
        Cases l1 of
              nil => l2 
     | (cons h t) => (cons  h (cat t l2))
end.


Theorem proofCatImpl : (l1,l2:List) { l:List |  (catP l1 l2 l) }.


Realizer cat.


Program.
Auto.