Require Export List.
Definition conca:forall A:Set,list A -> list A -> list A.
intros A primera segunda.
induction primera.
exact segunda.
clear primera.
exact (a::IHprimera).
Defined.

Implicit Arguments conca [A].

Definition ej1 := 1::2::3::nil.
Definition ej2:=4::5::nil.
Eval compute in (conca ej1 ej2).

Theorem compr_1:forall (A:Set) (l: list A), conca nil l = l.
simpl;trivial.
Qed.
Theorem compr_2:forall (A:Set)(l m:list A) (a:A), conca (a::l) m =
a::(conca l m).
simpl;trivial.
Qed.

Check list_rec.

Definition conc (A:Set):=(list_rec  (fun (_:list A)=>list A -> list A) 
(fun l:list A => l) (fun (a:A) (l: list A) (concl:list A-> list A) (l':list A) => (a::(concl l')))).

Implicit Arguments conc [A].
Eval compute in (conc ej1 ej2).

Theorem coinc: forall (A:Set) (l l' : list A), conca l l' = conc l l'.

induction l;simpl;trivial.
intros.
rewrite IHl.
trivial.
Qed.


