The Coq mailing list

[Gregory Bush <gbush AT mysck.com>]

Functional extensionality is a common axiom, and assuming it will  
prove eeq_congr, so I would not be worried it is inconsistent.  I  
suspect a model-theoretic argument is needed to prove eeq_congr is  
independent.  I'll leave that part to the experts.

--

Section aa.

Variables (A : Set).

Definition eeq (s t : nat -> A) :=
forall n, s n = t n.

Infix "==" := eeq  (at level 75, no associativity).

Axiom funext : forall A B (f g : A -> B) x, f x = g x -> f = g.

Lemma eeq_congr : forall f s t, s == t -> f s == f t.
unfold eeq.
intros.
assert (s = t).
apply funext with n; trivial.
destruct H0; trivial.
Qed.

On Nov 25, 2011, at 9:00 AM, Dimitri Hendriks wrote:

> Section aa.
>
> Variables (A : Set).
>
> Definition eeq (s t : nat -> A) :=
> forall n, s n = t n.
>
> Infix "==" := eeq  (at level 75, no associativity).
>
> Definition shift (s : nat -> A) :=
> fun n => s (S n).
>
> Lemma eeq_congr :
> forall f s t,
> s == t ->
> f s == f t.