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 ];
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 ];
[simplify;apply le_S_S;assumption
|simplify;apply le_S;assumption]]
qed.
\ No newline at end of file
[simplify;apply le_S_S;assumption
|simplify;apply le_S;assumption]]
qed.
\ No newline at end of file