intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl]
intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
qed.
lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl]
intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
qed.
lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];